:: deftheorem defines GCH CARD_FIL:def 12 :
( GCH iff for N being Aleph holds nextcard N = exp (2,N) );