let x be object ; :: thesis: card {x} = 1
A1: 1 = succ 0 ;
1 is cardinal
proof
take IT = 1; :: according to CARD_1:def 1 :: thesis: ( 1 = IT & ( for A being Ordinal st A,IT are_equipotent holds
IT c= A ) )
thus 1 = IT ; :: thesis: for A being Ordinal st A,IT are_equipotent holds
IT c= A
let A be Ordinal; :: thesis: ( A,IT are_equipotent implies IT c= A )
assume A,IT are_equipotent ; :: thesis: IT c= A
then ex y being object st A = {y} by A1, Th27;
hence IT c= A by A1, ZFMISC_1:33; :: thesis: verum
end;
then reconsider M = 1 as Cardinal ;
{x},M are_equipotent by A1, Th27;
hence card {x} = 1 by Def2; :: thesis: verum