now

let x be set ; :: thesis: ( x in RelIncl X implies x in [:X,X:] )
assume A1: x in RelIncl X ; :: thesis: x in [:X,X:]
then consider y, z being set such that
A2: x = [y,z] by RELAT_1:def 1;
( y in field (RelIncl X) & z in field (RelIncl X) ) by A1, A2, RELAT_1:30;
then ( y in X & z in X ) by WELLORD2:def 1;
hence x in [:X,X:] by A2, ZFMISC_1:106; :: thesis: verum

end;

then RelIncl X c= [:X,X:] by TARSKI:def 3;
then reconsider R = RelIncl X as Relation of X ;
A3: field R = X by WELLORD2:def 1;
R is reflexive by WELLORD2:2;
then R is_reflexive_in X by A3, RELAT_2:def 9;
then dom R = X by ORDERS_1:98;
hence RelIncl X is Order of X by PARTFUN1:def 4, WELLORD2:2, WELLORD2:3, WELLORD2:5; :: thesis: verum