:: deftheorem defines measurable CARD_FIL:def 16 :
for M being Aleph holds
( M is measurable iff ex Uf being Filter of M st
( Uf is_complete_with M & not Uf is principal & Uf is being_ultrafilter ) );