consider R' being Relation such that
A1: R' well_orders A by WELLORD2:26;
set R = R' |_2 A;
A2: ( field (R' |_2 A) = A & R' |_2 A is well-ordering ) by A1, WELLORD2:25;
R' |_2 A c= [:A,A:] by XBOOLE_1:17;
then reconsider R = R' |_2 A as Relation of A ;

now

let a be set ; :: thesis: ( a in A implies a in dom R )
assume A3: a in A ; :: thesis: a in dom R
R' is_reflexive_in A by A1, WELLORD1:def 5;
then ( [a,a] in R' & [a,a] in [:A,A:] ) by A3, RELAT_2:def 1, ZFMISC_1:def 2;
then [a,a] in R by XBOOLE_0:def 4;
hence a in dom R by RELAT_1:def 4; :: thesis: verum

end;

then A c= dom R by TARSKI:def 3;
then dom R = A by XBOOLE_0:def 10;
then reconsider R = R as Order of A by A2, PARTFUN1:def 4, WELLORD1:def 4;
take R ; :: thesis: R is connected
thus R is connected by A2, WELLORD1:def 4; :: thesis: verum