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;
b in field (RelIncl X) by A1, A2, RELAT_1:30;
then A3: b in X by WELLORD2:def 1;
a in field (RelIncl X) by A1, A2, RELAT_1:30;
then a in X by WELLORD2:def 1;
hence x in [:X,X:] by A2, A3, ZFMISC_1:106; :: thesis: verum