theorem Th11: :: WAYBEL22:11

for X being set
for F being Filter of (BoolePoset X) holds F = "\/" ( { ("/\" ( { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,(InclPoset (Filt (BoolePoset X))))) where Y is Subset of X : Y in F } ,(InclPoset (Filt (BoolePoset X))))