for n being Nat
for a being Aleph holds
( a <> 0 & a <> 1 & a <> 2 & a <> card n & card n in a & omega c= a )