let X be non empty set ; :: thesis: for A being Element of (BoolePoset X) holds { B where B is Element of (BoolePoset X) : A c= B } is Filter of (BoolePoset X)
let A be Element of (BoolePoset X); :: thesis: { B where B is Element of (BoolePoset X) : A c= B } is Filter of (BoolePoset X)
reconsider A = A as Subset of X by WAYBEL_8:26;
{ B where B is Element of (BoolePoset X) : A c= B } = { B where B is Subset of X : A c= B } by Th29;
hence { B where B is Element of (BoolePoset X) : A c= B } is Filter of (BoolePoset X) by Th30Thm70; :: thesis: verum