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 ;
hence ( card A in M implies A in M ) by Th43; :: thesis: verum