let X be set ; :: thesis: RelIncl X c= [:X,X:]
set R = RelIncl X;
let a, b be set ; :: according to RELAT_1:def 3 :: thesis: ( not [a,b] in RelIncl X or [a,b] in [:X,X:] )
assume A2: [a,b] in RelIncl X ; :: thesis: [a,b] in [:X,X:]
then b in field (RelIncl X) by RELAT_1:30;
then A3: b in X by Def1;
a in field (RelIncl X) by A2, RELAT_1:30;
then a in X by Def1;
hence [a,b] in [:X,X:] by A3, ZFMISC_1:106; :: thesis: verum