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 :: thesis: for a being object st a in A holds
a in dom R
let a be object ; :: 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;
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 XTUPLE_0:def 12; :: 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;
take R ; :: thesis: R is connected
thus R is connected by A2; :: thesis: verum