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

end;

then reconsider R = RelIncl X as Relation of X by TARSKI:def 3;
( field R = X & R is reflexive ) by WELLORD2:1, WELLORD2:def 1;
then R is_reflexive_in X by RELAT_2:def 9;
then dom R = X by ORDERS_1:13;
hence RelIncl X is Order of X by PARTFUN1:def 2, WELLORD2:1, WELLORD2:2, WELLORD2:4; :: thesis: verum