let X be set ; :: thesis: for N being Cardinal st N c= card X holds
ex Y being set st
( Y c= X & card Y = N )
X, card X are_equipotent by CARD_1:def 2;
then consider f being Function such that
A1: f is one-to-one and
A2: dom f = card X and
A3: rng f = X by WELLORD2:def 4;
let N be Cardinal; :: thesis: ( N c= card X implies ex Y being set st
( Y c= X & card Y = N ) )
assume N c= card X ; :: thesis: ex Y being set st
( Y c= X & card Y = N )
then A4: dom (f | N) = N by A2, RELAT_1:62;
take f .: N ; :: thesis: ( f .: N c= X & card (f .: N) = N )
thus f .: N c= X by A3, RELAT_1:111; :: thesis: card (f .: N) = N
A5: rng (f | N) = f .: N by RELAT_1:115;
f | N is one-to-one by A1, FUNCT_1:52;
then N,f .: N are_equipotent by A4, A5, WELLORD2:def 4;
hence card (f .: N) = N by CARD_1:def 2; :: thesis: verum