let X be set ; :: thesis: RelIncl X c= [:X,X:]
set R = RelIncl X;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in RelIncl X or x in [:X,X:] )
assume A1: x in RelIncl X ; :: thesis: x in [:X,X:]
then consider a, b being set such that
A2: x = [a,b] by RELAT_1:def 1;
( a in field (RelIncl X) & b in field (RelIncl X) ) by A1, A2, RELAT_1:30;
then ( a in X & b in X ) by WELLORD2:def 1;
hence x in [:X,X:] by A2, ZFMISC_1:106; :: thesis: verum