now :: thesis: for x being object st x in RelIncl X holds
x in [:X,X:]
let x be object ; :: 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 object 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:def 1;
then R is_reflexive_in X ;
then dom R = X by Th13;
hence RelIncl X is Order of X by PARTFUN1:def 2; :: thesis: verum