let R be Relation; :: thesis: ( R is well-ordering implies field R, order_type_of R are_equipotent )
assume R is well-ordering ; :: thesis: field R, order_type_of R are_equipotent
then R, RelIncl (order_type_of R) are_isomorphic by WELLORD2:def 2;
then consider f being Function such that
A1: f is_isomorphism_of R, RelIncl (order_type_of R) by WELLORD1:def 8;
take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & dom f = field R & rng f = order_type_of R )
field (RelIncl (order_type_of R)) = order_type_of R by WELLORD2:def 1;
hence ( f is one-to-one & dom f = field R & rng f = order_type_of R ) by A1, WELLORD1:def 7; :: thesis: verum