theorem Th16: :: WAYBEL22:16

for X being set holds FixedUltraFilters X is_FreeGen_set_of InclPoset (Filt (BoolePoset X))