:: deftheorem defines FixedUltraFilters WAYBEL22:def 2 :
for X being set holds FixedUltraFilters X = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } ;