let X be set ; :: thesis: for x being Element of (BoolePoset X) holds compactbelow x = { y where y is finite Subset of x : verum }
let x be Element of (BoolePoset X); :: thesis: compactbelow x = { y where y is finite Subset of x : verum }

now :: thesis: for z being set st z in { y where y is finite Subset of x : verum } holds
z in compactbelow x

let z be set ; :: thesis: ( z in { y where y is finite Subset of x : verum } implies z in compactbelow x )
assume z in { y where y is finite Subset of x : verum } ; :: thesis: z in compactbelow x
then consider z9 being finite Subset of x such that
A1: z9 = z ;
x c= X by Th26;
then z9 c= X by XBOOLE_1:1;
then reconsider z1 = z9 as Element of (BoolePoset X) by Th26;
( z1 is compact & z1 <= x ) by Th28, YELLOW_1:2;
hence z in compactbelow x by A1; :: thesis: verum

end;

then A2: { y where y is finite Subset of x : verum } c= compactbelow x by TARSKI:def 3;

now :: thesis: for z being set st z in compactbelow x holds
z in { y where y is finite Subset of x : verum }

let z be set ; :: thesis: ( z in compactbelow x implies z in { y where y is finite Subset of x : verum } )
assume z in compactbelow x ; :: thesis: z in { y where y is finite Subset of x : verum }
then consider z9 being Element of (BoolePoset X) such that
A3: z9 = z and
A4: ( x >= z9 & z9 is compact ) ;
( z is finite & z9 c= x ) by A3, A4, Th28, YELLOW_1:2;
hence z in { y where y is finite Subset of x : verum } by A3; :: thesis: verum

end;

then compactbelow x c= { y where y is finite Subset of x : verum } by TARSKI:def 3;
hence compactbelow x = { y where y is finite Subset of x : verum } by A2, XBOOLE_0:def 10; :: thesis: verum