:: deftheorem defines strongly_inaccessible CARD_FIL:def 15 :
for IT being Aleph holds
( IT is strongly_inaccessible iff ( IT is regular & IT is strong_limit ) );