let R be non empty Poset; ( the InternalRel of R well_orders the carrier of R iff for N being non empty Subset of R holds card (min-classes N) = 1 )
set IR = the InternalRel of R;
set CR = the carrier of R;
A1:
R is quasi_ordered
;
assume A7:
for N being non empty Subset of R holds card (min-classes N) = 1
; the InternalRel of R well_orders the carrier of R
then A8:
R is connected
by A1, Th22;
A9:
R \~ is well_founded
by A1, A7, Th22;
A10:
the InternalRel of R is_strongly_connected_in the carrier of R
by A8, Th4;
A11:
R is well_founded
by A9, Th15;
A12:
the InternalRel of R is_reflexive_in the carrier of R
by ORDERS_2:def 2;
A13:
the InternalRel of R is_transitive_in the carrier of R
by ORDERS_2:def 3;
A14:
the InternalRel of R is_antisymmetric_in the carrier of R
by ORDERS_2:def 4;
A15:
the InternalRel of R is_connected_in the carrier of R
by A10;
the InternalRel of R is_well_founded_in the carrier of R
by A11, WELLFND1:def 2;
hence
the InternalRel of R well_orders the carrier of R
by A12, A13, A14, A15, WELLORD1:def 5; verum