A7:
field (RelIncl X) = X
by Def1;

let a, b be object ; :: according to RELAT_2:def 4,RELAT_2:def 12 :: thesis: ( not a in field (RelIncl X) or not b in field (RelIncl X) or not [a,b] in RelIncl X or not [b,a] in RelIncl X or a = b )

assume A8: ( a in field (RelIncl X) & b in field (RelIncl X) & [a,b] in RelIncl X & [b,a] in RelIncl X ) ; :: thesis: a = b

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

( a c= b & b c= a ) by A7, Def1, A8;

hence a = b by XBOOLE_0:def 10; :: thesis: verum

let a, b be object ; :: according to RELAT_2:def 4,RELAT_2:def 12 :: thesis: ( not a in field (RelIncl X) or not b in field (RelIncl X) or not [a,b] in RelIncl X or not [b,a] in RelIncl X or a = b )

assume A8: ( a in field (RelIncl X) & b in field (RelIncl X) & [a,b] in RelIncl X & [b,a] in RelIncl X ) ; :: thesis: a = b

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

( a c= b & b c= a ) by A7, Def1, A8;

hence a = b by XBOOLE_0:def 10; :: thesis: verum