let A be Ordinal; for X being set st X c= A holds
card X = card (order_type_of (RelIncl X))
let X be set ; ( X c= A implies card X = card (order_type_of (RelIncl X)) )
set R = RelIncl X;
set B = order_type_of (RelIncl X);
set phi = canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X));
assume
X c= A
; card X = card (order_type_of (RelIncl X))
then
RelIncl X is well-ordering
by WELLORD2:8;
then
RelIncl X, RelIncl (order_type_of (RelIncl X)) are_isomorphic
by WELLORD2:def 2;
then
( RelIncl (order_type_of (RelIncl X)) is well-ordering & RelIncl (order_type_of (RelIncl X)), RelIncl X are_isomorphic )
by WELLORD1:40, WELLORD2:8;
then A1:
canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) is_isomorphism_of RelIncl (order_type_of (RelIncl X)), RelIncl X
by WELLORD1:def 9;
field (RelIncl X) = X
by WELLORD2:def 1;
then A2:
rng (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) = X
by A1, WELLORD1:def 7;
field (RelIncl (order_type_of (RelIncl X))) = order_type_of (RelIncl X)
by WELLORD2:def 1;
then A3:
dom (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X))) = order_type_of (RelIncl X)
by A1, WELLORD1:def 7;
canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) is one-to-one
by A1, WELLORD1:def 7;
then
order_type_of (RelIncl X),X are_equipotent
by A3, A2, WELLORD2:def 4;
hence
card X = card (order_type_of (RelIncl X))
by CARD_1:5; verum