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