let a, b, c be object ; RELAT_2:def 8,RELAT_2:def 16 ( 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 )
; [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; verum