let a, b, c be object ; :: according to RELAT_2:def 8,RELAT_2:def 16 :: thesis: ( not a in field the InternalRel of R or not b in field the InternalRel of R or not c in field the InternalRel of R or not [a,b] in the InternalRel of R or not [b,c] in the InternalRel of R or [a,c] in the InternalRel of R )
assume A1: ( a in field the InternalRel of R & b in field the InternalRel of R & c in field the InternalRel of R ) ; :: thesis: ( not [a,b] in the InternalRel of R or not [b,c] in the InternalRel of R or [a,c] in the InternalRel of R )
field the InternalRel of R c= the carrier of R \/ the carrier of R by RELSET_1:8;
hence ( not [a,b] in the InternalRel of R or not [b,c] in the InternalRel of R or [a,c] in the InternalRel of R ) by A1, RELAT_2:def 8, ORDERS_2:def 3; :: thesis: verum