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