theorem :: CARDFIL2:69

for X being non empty set
for A being Element of (BoolePoset X) holds { B where B is Element of (BoolePoset X) : A c= B } is Filter of (BoolePoset X)