let X be non empty set ; :: thesis: for A being Element of (BoolePoset X) holds { Y where Y is Subset of X : A c= Y } is Filter of (BoolePoset X)
let A be Element of (BoolePoset X); :: thesis: { Y where Y is Subset of X : A c= Y } is Filter of (BoolePoset X)
{ Y where Y is Subset of X : A c= Y } = uparrow A by WAYBEL15:2;
hence { Y where Y is Subset of X : A c= Y } is Filter of (BoolePoset X) ; :: thesis: verum