theorem :: DICKSON:24

for R being non empty Poset holds
( 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 )