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