let L be non empty reflexive RelStr ; :: thesis: for x being Element of L holds compactbelow x is Subset of (CompactSublatt L)
let x be Element of L; :: thesis: compactbelow x is Subset of (CompactSublatt L)

now

let v be set ; :: thesis: ( v in compactbelow x implies v in the carrier of (CompactSublatt L) )
assume v in compactbelow x ; :: thesis: v in the carrier of (CompactSublatt L)
then v in { z where z is Element of L : ( x >= z & z is compact ) } by WAYBEL_8:def 2;
then consider v1 being Element of L such that
A1: v1 = v and
x >= v1 and
A2: v1 is compact ;
thus v in the carrier of (CompactSublatt L) by A1, A2, WAYBEL_8:def 1; :: thesis: verum

end;

hence compactbelow x is Subset of (CompactSublatt L) by TARSKI:def 3; :: thesis: verum