:: deftheorem defines ultra WAYBEL_7:def 3 :
for L being non empty Poset
for F being Filter of L holds
( F is ultra iff ( F is proper & ( for G being Filter of L holds
( not F c= G or F = G or G = the carrier of L ) ) ) );