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 ;
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 A2: 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 A3: the InternalRel of R is_reflexive_in the carrier of R by WELLORD1:def 5;
A4: the InternalRel of R is_connected_in the carrier of R by A2, WELLORD1:def 5;
A5: the InternalRel of R is_well_founded_in the carrier of R by A2, WELLORD1:def 5;
the InternalRel of R is_strongly_connected_in the carrier of R by A3, A4, ORDERS_1:7;
then A6: R is connected by Th4;
R is well_founded by A5, WELLFND1:def 2;
then R \~ is well_founded by Th14;
hence for N being non empty Subset of R holds card (min-classes N) = 1 by A1, A6, Th22; :: thesis: verum
end;
assume A7: 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 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; :: thesis: verum