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 :: thesis: for v being object st v in compactbelow x holds
v in the carrier of (CompactSublatt L)

let v be object ; :: 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 ex v1 being Element of L st
( v1 = v & x >= v1 & v1 is compact ) ;
hence v in the carrier of (CompactSublatt L) by WAYBEL_8:def 1; :: thesis: verum

end;

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