let R be non empty Poset; :: thesis: ( 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 by Def3;

hereby :: thesis: ( ( for N being non empty Subset of R holds card (min-classes N) = 1 ) implies the InternalRel of R well_orders the carrier of R )

assume the InternalRel of R well_orders the carrier of R ; :: thesis: for N being non empty Subset of R holds card (min-classes N) = 1
then A2: ( the InternalRel of R is_reflexive_in the carrier of R & the InternalRel of R is_transitive_in the carrier of R & the InternalRel of R is_antisymmetric_in the carrier of R & the InternalRel of R is_connected_in the carrier of R & the InternalRel of R is_well_founded_in the carrier of R ) by WELLORD1:def 5;
then the InternalRel of R is_strongly_connected_in the carrier of R by ORDERS_1:92;
then A3: R is connected by Th5;
R is well_founded by A2, WELLFND1:def 2;
then R \~ is well_founded by Th16;
hence for N being non empty Subset of R holds card (min-classes N) = 1 by A1, A3, Th24; :: thesis: verum

end;

assume for N being non empty Subset of R holds card (min-classes N) = 1 ; :: thesis: the InternalRel of R well_orders the carrier of R
then A4: ( R is connected & R \~ is well_founded ) by A1, Th24;

now

thus the InternalRel of R is_reflexive_in the carrier of R by ORDERS_2:def 4; :: thesis: ( the InternalRel of R is_transitive_in the carrier of R & the InternalRel of R is_antisymmetric_in the carrier of R & the InternalRel of R is_connected_in the carrier of R & the InternalRel of R is_well_founded_in the carrier of R )
thus the InternalRel of R is_transitive_in the carrier of R by ORDERS_2:def 5; :: thesis: ( the InternalRel of R is_antisymmetric_in the carrier of R & the InternalRel of R is_connected_in the carrier of R & the InternalRel of R is_well_founded_in the carrier of R )
thus the InternalRel of R is_antisymmetric_in the carrier of R by ORDERS_2:def 6; :: thesis: ( the InternalRel of R is_connected_in the carrier of R & the InternalRel of R is_well_founded_in the carrier of R )
the InternalRel of R is_strongly_connected_in the carrier of R by A4, Th5;
hence the InternalRel of R is_connected_in the carrier of R by ORDERS_1:92; :: thesis: the InternalRel of R is_well_founded_in the carrier of R
R is well_founded by A4, Th17;
hence the InternalRel of R is_well_founded_in the carrier of R by WELLFND1:def 2; :: thesis: verum

end;

hence the InternalRel of R well_orders the carrier of R by WELLORD1:def 5; :: thesis: verum