theorem :: CARDFIL2:70

for X being non empty set
for B being non empty Subset of (BoolePoset X) holds
( ( for x, y being Element of B ex z being Element of B st z c= x /\ y ) iff B is filtered )