let R, S be Relation; :: thesis: for F being Function st R is well-ordering & F is_isomorphism_of R,S holds
S is well-ordering
let F be Function; :: thesis: ( R is well-ordering & F is_isomorphism_of R,S implies S is well-ordering )
assume ( R is reflexive & R is transitive & R is antisymmetric & R is connected & R is well_founded & F is_isomorphism_of R,S ) ; :: according to WELLORD1:def 4 :: thesis: S is well-ordering
hence ( S is reflexive & S is transitive & S is antisymmetric & S is connected & S is well_founded ) by Th53; :: according to WELLORD1:def 4 :: thesis: verum