let X be set ; :: thesis:
let A be Subset of X; :: thesis:
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:

hereby :: thesis:

let x be object ; :: thesis:
assume x in { B where B is Element of (BoolePoset X) : A c= B } ; :: thesis:
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:

end;

let x be object ; :: thesis:
assume x in { B where B is Subset of X : A c= B } ; :: thesis:
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:

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: