let X be set ; :: thesis: RelIncl X is antisymmetric
let a be set ; :: according to RELAT_2:def 4,RELAT_2:def 12 :: thesis: for b₁ being set holds
( 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₁ )
let b be set ; :: 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 A1: ( a in field (RelIncl X) & b in field (RelIncl X) & [a,b] in RelIncl X & [b,a] in RelIncl X ) ; :: thesis: a = b
( field (RelIncl X) = X & ( for Y, Z being set st Y in X & Z in X holds
( [Y,Z] in RelIncl X iff Y c= Z ) ) ) by Def1;
then ( a c= b & b c= a ) by A1;
hence a = b by XBOOLE_0:def 10; :: thesis: verum