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

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