let X be set ; :: thesis:

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

A1: now :: thesis:

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

let t be object ; :: thesis:
assume A3: t in x ; :: thesis:
A4: x c= X by Th26;

let k be object ; :: thesis:
assume k in {t} ; :: thesis:
then k = t by TARSKI:def 1;
hence k in X by A3, A4; :: thesis:

end;

then {t} c= X ;
then reconsider t1 = {t} as Element of (BoolePoset X) by Th26;
for k being object 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 Th29;
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:

end;

then x c= a ;
hence x <= a by YELLOW_1:2; :: thesis:

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:

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 ) ;
hence BoolePoset X is algebraic ; :: thesis: