let A be Ordinal; :: thesis: for X being set st X c= A holds
card X = card (order_type_of (RelIncl X))
let X be set ; :: thesis: ( 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 ; :: thesis: card X = card (order_type_of (RelIncl X))
then A1: ( RelIncl X is well-ordering & RelIncl (order_type_of (RelIncl X)) is well-ordering & order_type_of (RelIncl X) c= A ) by WELLORD2:9, WELLORD2:17;
then RelIncl X, RelIncl (order_type_of (RelIncl X)) are_isomorphic by WELLORD2:def 2;
then RelIncl (order_type_of (RelIncl X)), RelIncl X are_isomorphic by WELLORD1:50;
then ( canonical_isomorphism_of (RelIncl (order_type_of (RelIncl X))),(RelIncl X) is_isomorphism_of RelIncl (order_type_of (RelIncl X)), RelIncl X & field (RelIncl (order_type_of (RelIncl X))) = order_type_of (RelIncl X) & field (RelIncl X) = X ) by A1, WELLORD1:def 9, WELLORD2:def 1;
then ( dom (canonical_isomorphism_of (RelIncl (order_type_of (RelIncl X))),(RelIncl X)) = order_type_of (RelIncl X) & rng (canonical_isomorphism_of (RelIncl (order_type_of (RelIncl X))),(RelIncl X)) = X & canonical_isomorphism_of (RelIncl (order_type_of (RelIncl X))),(RelIncl X) is one-to-one & ( for x, y being set holds
( [x,y] in RelIncl (order_type_of (RelIncl X)) iff ( x in order_type_of (RelIncl X) & y in order_type_of (RelIncl X) & [((canonical_isomorphism_of (RelIncl (order_type_of (RelIncl X))),(RelIncl X)) . x),((canonical_isomorphism_of (RelIncl (order_type_of (RelIncl X))),(RelIncl X)) . y)] in RelIncl X ) ) ) ) by WELLORD1:def 7;
then order_type_of (RelIncl X),X are_equipotent by WELLORD2:def 4;
hence card X = card (order_type_of (RelIncl X)) by CARD_1:21; :: thesis: verum