set F = the proper Filter of (BoolePoset X);
ex G being Filter of (BoolePoset X) st
( the proper Filter of (BoolePoset X) c= G & G is ultra ) by Th26;
hence ex b₁ being Filter of (BoolePoset X) st b₁ is ultra ; :: thesis: verum