let R, S be Relation; :: thesis: ( R,S are_isomorphic & R is well-ordering implies S is well-ordering )
assume R,S are_isomorphic ; :: thesis: ( not R is well-ordering or S is well-ordering )
then ex F being Function st F is_isomorphism_of R,S by WELLORD1:def 8;
hence ( not R is well-ordering or S is well-ordering ) by WELLORD1:54; :: thesis: verum