let X be set ; :: thesis: BoolePoset X is algebraic
A1: for x being Element of (BoolePoset X) holds
( not compactbelow x is empty & compactbelow x is directed ) ;

now

let x be Element of (BoolePoset X); :: thesis: x = sup (compactbelow x)
for b being Element of (BoolePoset X) st b in compactbelow x holds
b <= x by Th4;
then A2: x is_>=_than compactbelow x by LATTICE3:def 9;

now

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

now

let t be set ; :: thesis: ( t in x implies t in a )
A4: t in {t} by TARSKI:def 1;
assume A5: t in x ; :: thesis: t in a
A6: 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 A5, A6; :: 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 A5, 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 A3, LATTICE3:def 9;
then {t} c= a by YELLOW_1:2;
hence t in a by A4; :: thesis: verum

end;

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

end;

hence x = sup (compactbelow x) by A2, YELLOW_0:32; :: thesis: verum

end;

then BoolePoset X is satisfying_axiom_K by Def3;
hence BoolePoset X is algebraic by A1, Def4; :: thesis: verum