let X be set ; :: thesis: FixedUltraFilters X c= Filt (BoolePoset X)
let F be object ; :: according to TARSKI:def 3 :: thesis: ( not F in FixedUltraFilters X or F in Filt (BoolePoset X) )
assume F in FixedUltraFilters X ; :: thesis: F in Filt (BoolePoset X)
then ex x being Element of (BoolePoset X) st
( F = uparrow x & ex y being Element of X st x = {y} ) ;
hence F in Filt (BoolePoset X) ; :: thesis: verum