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 )

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

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 & R is transitive & R is antisymmetric & R is connected & R is well_founded )
; :: according to WELLORD1:def 4 :: thesis: R well_orders field R
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;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

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