consider R' being Relation such that
A1:
R' well_orders A
by WELLORD2:26;
set R = R' |_2 A;
A2:
R' |_2 A is well-ordering
by A1, WELLORD2:25;
reconsider R = R' |_2 A as Relation of by XBOOLE_1:17;
A3:
now let a be
set ;
( a in A implies a in dom R )assume A4:
a in A
;
a in dom RA5:
R' is_reflexive_in A
by A1, WELLORD1:def 5;
A6:
[a,a] in R'
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;
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 by A2, A10, PARTFUN1:def 4, WELLORD1:def 4;
take
R
; R is connected
thus
R is connected
by A2, WELLORD1:def 4; verum