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 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; :: thesis: verum