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

A3: now

let a be set ; :: thesis: ( a in A implies a in dom R )
assume A4: a in A ; :: thesis: a in dom R
A5: R9 is_reflexive_in A by A1, WELLORD1:def 5;
A6: [a,a] in R9 by A4, A5, RELAT_2:def 1;
A7: [a,a] in [:A,A:] by A4, ZFMISC_1:def 2;
A8: [a,a] in R by A6, A7, XBOOLE_0:def 4;
thus a in dom R by A8, RELAT_1:def 4; :: thesis: verum

end;

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