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;

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

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

then
A c= dom R
by TARSKI:def 3;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;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

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