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 :: thesis: for b being Element of (BoolePoset X) st b is_>=_than Y holds
Un <= b

let b be Element of (BoolePoset X); :: thesis: ( b is_>=_than Y implies Un <= b )
assume A3: b is_>=_than Y ; :: thesis: Un <= b
for Z being set st Z in Y holds
Z c= b by Th2, A3;
then Un c= b by ZFMISC_1:76;
hence Un <= b by Th2; :: thesis: verum

end;

for b being Element of (BoolePoset X) st b in Y holds
b <= Un by Th2, ZFMISC_1:74;
then Un is_>=_than Y ;
hence sup Y = union Y by A2, YELLOW_0:30; :: thesis: verum