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 )
card M = M by CARD_1:def 2;
hence ( card A in M implies A in M ) by Th59; :: thesis: verum