let S be set ; :: thesis: ( S is empty implies S is cardinal )
assume A1: S is empty ; :: thesis: S is cardinal
take {} ; :: according to CARD_1:def 1 :: thesis: ( S = {} & ( for A being Ordinal st A, {} are_equipotent holds
{} c= A ) )
thus S = {} by A1; :: thesis: for A being Ordinal st A, {} are_equipotent holds
{} c= A
let A be Ordinal; :: thesis: ( A, {} are_equipotent implies {} c= A )
assume A, {} are_equipotent ; :: thesis: {} c= A
thus {} c= A ; :: thesis: verum