let n be Nat; :: thesis: for a being Aleph holds
( a <> 0 & a <> 1 & a <> 2 & a <> card n & card n in a & omega c= a )
let a be Aleph; :: thesis: ( a <> 0 & a <> 1 & a <> 2 & a <> card n & card n in a & omega c= a )
( omega c= a & card n in omega ) by CARD_3:85;
hence ( a <> 0 & a <> 1 & a <> 2 & a <> card n & card n in a & omega c= a ) ; :: thesis: verum