(subclass TotalOrderingRelation PartialOrderingRelation) | Merge.kif 2374-2374 | 子類 TotalOrderingRelation and PartialOrderingRelation |
(subclass TotalOrderingRelation TrichotomizingRelation) | Merge.kif 2375-2375 | 子類 TotalOrderingRelation and TrichotomizingRelation |