let A be Ordinal; :: thesis: for M being Cardinal st card A in M holds
A in M
let M be Cardinal; :: thesis: ( card A in M implies A in M )
( M = M & card M = M ) by CARD_1:def 5;
hence ( card A in M implies A in M ) by Th59; :: thesis: verum