let X be set ; :: thesis: for Y being Subset of (BoolePoset X) holds sup Y = union Y
set L = BoolePoset X;
let Y be Subset of (BoolePoset X); :: thesis: sup Y = union Y
A1: the carrier of (BoolePoset X) = bool X by LATTICE3:def 1;
then union Y c= union (bool X) by ZFMISC_1:77;
then reconsider Un = union Y as Element of (BoolePoset X) by A1, ZFMISC_1:81;

A2: now

let b be Element of (BoolePoset X); :: thesis: ( b is_>=_than Y implies Un <= b )
assume A3: b is_>=_than Y ; :: thesis: Un <= b

now

let Z be set ; :: thesis: ( Z in Y implies Z c= b )
assume A4: Z in Y ; :: thesis: Z c= b
then reconsider Z9 = Z as Element of (BoolePoset X) ;
Z9 <= b by A3, A4, LATTICE3:def 9;
hence Z c= b by Th2; :: thesis: verum

end;

then Un c= b by ZFMISC_1:76;
hence Un <= b by Th2; :: thesis: verum

end;

now

let b be Element of (BoolePoset X); :: thesis: ( b in Y implies b <= Un )
assume b in Y ; :: thesis: b <= Un
then b c= Un by ZFMISC_1:74;
hence b <= Un by Th2; :: thesis: verum

end;

then Un is_>=_than Y by LATTICE3:def 9;
hence sup Y = union Y by A2, YELLOW_0:30; :: thesis: verum