let X be set ; :: thesis: for A being Subset of X holds { B where B is Element of (BoolePoset X) : A c= B } = uparrow (PLO2bis A)
let A be Subset of X; :: thesis: { B where B is Element of (BoolePoset X) : A c= B } = uparrow (PLO2bis A)
reconsider Z = PLO2bis A as Element of (BoolePoset X) ;
set S1 = { Y where Y is Subset of X : Z c= Y } ;
set S2 = { B where B is Subset of X : A c= B } ;
{ 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 } = uparrow (PLO2bis A) by WAYBEL15:2; :: thesis: verum