consider R9 being Relation such that
A1: R9 well_orders A by WELLORD2:17;
set R = R9 |_2 A;
A2: R9 |_2 A is well-ordering by A1, WELLORD2:16;
reconsider R = R9 |_2 A as Relation of A by XBOOLE_1:17;

now

let a be set ; :: thesis: ( a in A implies a in dom R )
assume A3: a in A ; :: thesis: a in dom R
R9 is_reflexive_in A by A1, WELLORD1:def 5;
then A4: [a,a] in R9 by A3, RELAT_2:def 1;
[a,a] in [:A,A:] by A3, ZFMISC_1:def 2;
then [a,a] in R by A4, 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 2, WELLORD1:def 4;
take R ; :: thesis: R is connected
thus R is connected by A2, WELLORD1:def 4; :: thesis: verum