let a, b, c be object ; :: according to RELAT_2:def 8,RELAT_2:def 16 :: thesis: ( not a in field (RelIncl X) or not b in field (RelIncl X) or not c in field (RelIncl X) or not [a,b] in RelIncl X or not [b,c] in RelIncl X or [a,c] in RelIncl X )

assume that

A2: a in field (RelIncl X) and

A3: b in field (RelIncl X) and

A4: c in field (RelIncl X) and

A5: ( [a,b] in RelIncl X & [b,c] in RelIncl X ) ; :: thesis: [a,c] in RelIncl X

reconsider a = a, b = b, c = c as set by TARSKI:1;

field (RelIncl X) = X by Def1;

then ( a c= b & b c= c ) by A2, A3, A4, A5, Def1;

then A6: a c= c ;

( a in X & c in X ) by A2, A4, Def1;

hence [a,c] in RelIncl X by A6, Def1; :: thesis: verum

assume that

A2: a in field (RelIncl X) and

A3: b in field (RelIncl X) and

A4: c in field (RelIncl X) and

A5: ( [a,b] in RelIncl X & [b,c] in RelIncl X ) ; :: thesis: [a,c] in RelIncl X

reconsider a = a, b = b, c = c as set by TARSKI:1;

field (RelIncl X) = X by Def1;

then ( a c= b & b c= c ) by A2, A3, A4, A5, Def1;

then A6: a c= c ;

( a in X & c in X ) by A2, A4, Def1;

hence [a,c] in RelIncl X by A6, Def1; :: thesis: verum