let X be set ; :: thesis: BoolePoset X is algebraic

now

let x be Element of (BoolePoset X); :: thesis: x = sup (compactbelow x)

A1: now

let a be Element of (BoolePoset X); :: thesis: ( a is_>=_than compactbelow x implies x <= a )
assume A2: a is_>=_than compactbelow x ; :: thesis: x <= a

now

let t be set ; :: thesis: ( t in x implies t in a )
assume A3: t in x ; :: thesis: t in a
A4: x c= X by Th28;

now

let k be set ; :: thesis: ( k in {t} implies k in X )
assume k in {t} ; :: thesis: k in X
then k = t by TARSKI:def 1;
hence k in X by A3, A4; :: thesis: verum

end;

then {t} c= X by TARSKI:def 3;
then reconsider t1 = {t} as Element of (BoolePoset X) by Th28;
for k being set st k in {t} holds
k in x by A3, TARSKI:def 1;
then {t} is finite Subset of x by TARSKI:def 3;
then {t} in { y where y is finite Subset of x : verum } ;
then {t} in compactbelow x by Th31;
then t1 <= a by A2, LATTICE3:def 9;
then ( t in {t} & {t} c= a ) by TARSKI:def 1, YELLOW_1:2;
hence t in a ; :: thesis: verum

end;

then x c= a by TARSKI:def 3;
hence x <= a by YELLOW_1:2; :: thesis: verum

end;

for b being Element of (BoolePoset X) st b in compactbelow x holds
b <= x by Th4;
then x is_>=_than compactbelow x by LATTICE3:def 9;
hence x = sup (compactbelow x) by A1, YELLOW_0:32; :: thesis: verum

end;

then ( ( for x being Element of (BoolePoset X) holds
( not compactbelow x is empty & compactbelow x is directed ) ) & BoolePoset X is satisfying_axiom_K ) by Def3;
hence BoolePoset X is algebraic by Def4; :: thesis: verum