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

now :: thesis: for x being Element of (BoolePoset X) holds x = sup (compactbelow x)

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

A1: now :: thesis: for a being Element of (BoolePoset X) st a is_>=_than compactbelow x holds
x <= a

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 :: thesis: for t being object st t in x holds
t in a

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

now :: thesis: for k being object st k in {t} holds
k in X

let k be object ; :: 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 ;
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: verum

end;

then x c= a ;
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 ) ;
hence BoolePoset X is algebraic ; :: thesis: verum