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

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 z' being Element of (BoolePoset X) such that
A1: ( z' = z & x >= z' & z' is compact ) ;
A2: z is finite by A1, Th30;
z' c= x by A1, YELLOW_1:2;
hence z in { y where y is finite Subset of x : verum } by A1, A2; :: thesis: verum

end;

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

now

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 z' being finite Subset of x such that
A4: z' = z ;
x c= X by Th28;
then z' c= X by XBOOLE_1:1;
then reconsider z1 = z' as Element of (BoolePoset X) by Th28;
A5: z1 is compact by Th30;
z1 <= x by YELLOW_1:2;
hence z in compactbelow x by A4, A5; :: thesis: verum

end;

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