let R be Relation; :: thesis: ( R well_orders field R iff R is well-ordering )
thus ( R well_orders field R implies R is well-ordering ) :: thesis: ( R is well-ordering implies R well_orders field R )
proof
assume ( R is_reflexive_in field R & R is_transitive_in field R & R is_antisymmetric_in field R & R is_connected_in field R & R is_well_founded_in field R ) ; :: according to WELLORD1:def 5 :: thesis: R is well-ordering
hence ( R is reflexive & R is transitive & R is antisymmetric & R is connected & R is well_founded ) by RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 14, RELAT_2:def 16; :: according to WELLORD1:def 4 :: thesis: verum
end;
assume ( R is reflexive & R is transitive & R is antisymmetric & R is connected & R is well_founded ) ; :: according to WELLORD1:def 4 :: thesis: R well_orders field R
hence ( R is_reflexive_in field R & R is_transitive_in field R & R is_antisymmetric_in field R & R is_connected_in field R & R is_well_founded_in field R ) by RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 14, RELAT_2:def 16; :: according to WELLORD1:def 5 :: thesis: verum