let X be set ; :: thesis: RelIncl X is antisymmetric
A1: field (RelIncl X) = X by Def1;
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 ( a in field (RelIncl X) & b in field (RelIncl X) & [a,b] in RelIncl X & [b,a] in RelIncl X ) ; :: thesis: a = b
then ( a c= b & b c= a ) by A1, Def1;
hence a = b by XBOOLE_0:def 10; :: thesis: verum