let X be set ; :: thesis: for A being Subset of X holds { B where B is Element of (BoolePoset X) : A c= B } = { B where B is Subset of X : A c= B }
let A be Subset of X; :: thesis: { B where B is Element of (BoolePoset X) : A c= B } = { B where B is Subset of X : A c= B }
set C = { B where B is Element of (BoolePoset X) : A c= B } ;
set D = { B where B is Subset of X : A c= B } ;

now :: thesis: ( ( for x being object st x in { B where B is Element of (BoolePoset X) : A c= B } holds
x in { B where B is Subset of X : A c= B } ) & ( for x being object st x in { B where B is Subset of X : A c= B } holds
x in { B where B is Element of (BoolePoset X) : A c= B } ) )

hereby :: thesis: for x being object st x in { B where B is Subset of X : A c= B } holds
x in { B where B is Element of (BoolePoset X) : A c= B }

let x be object ; :: thesis: ( x in { B where B is Element of (BoolePoset X) : A c= B } implies x in { B where B is Subset of X : A c= B } )
assume x in { B where B is Element of (BoolePoset X) : A c= B } ; :: thesis: x in { B where B is Subset of X : A c= B }
then consider b0 being Element of (BoolePoset X) such that
A1: x = b0 and
A2: A c= b0 ;
x is Subset of X by A1, WAYBEL_8:26;
hence x in { B where B is Subset of X : A c= B } by A1, A2; :: thesis: verum

end;

let x be object ; :: thesis: ( x in { B where B is Subset of X : A c= B } implies x in { B where B is Element of (BoolePoset X) : A c= B } )
assume x in { B where B is Subset of X : A c= B } ; :: thesis: x in { B where B is Element of (BoolePoset X) : A c= B }
then consider b0 being Subset of X such that
A3: x = b0 and
A4: A c= b0 ;
x is Element of (BoolePoset X) by A3, WAYBEL_8:26;
hence x in { B where B is Element of (BoolePoset X) : A c= B } by A3, A4; :: thesis: verum

end;

then ( { B where B is Element of (BoolePoset X) : A c= B } c= { B where B is Subset of X : A c= B } & { B where B is Subset of X : A c= B } c= { B where B is Element of (BoolePoset X) : A c= B } ) ;
hence { B where B is Element of (BoolePoset X) : A c= B } = { B where B is Subset of X : A c= B } ; :: thesis: verum