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

now

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

end;

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

now

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

end;

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