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

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