let L be non empty reflexive RelStr ; :: thesis: for x being Element of L holds compactbelow x = (downarrow x) /\ the carrier of (CompactSublatt L)
let x be Element of L; :: thesis: compactbelow x = (downarrow x) /\ the carrier of (CompactSublatt L)

now

let y be set ; :: thesis: ( y in (downarrow x) /\ the carrier of (CompactSublatt L) implies y in compactbelow x )
assume A1: y in (downarrow x) /\ the carrier of (CompactSublatt L) ; :: thesis: y in compactbelow x
then A2: ( y in downarrow x & y in the carrier of (CompactSublatt L) ) by XBOOLE_0:def 4;
reconsider y' = y as Element of L by A1;
( y' <= x & y' is compact ) by A2, Def1, WAYBEL_0:17;
hence y in compactbelow x ; :: thesis: verum

end;

then A3: (downarrow x) /\ the carrier of (CompactSublatt L) c= compactbelow x by TARSKI:def 3;

now

let y be set ; :: thesis: ( y in compactbelow x implies y in (downarrow x) /\ the carrier of (CompactSublatt L) )
assume y in compactbelow x ; :: thesis: y in (downarrow x) /\ the carrier of (CompactSublatt L)
then consider y' being Element of L such that
A4: ( y' = y & y' <= x & y' is compact ) ;
( y' in downarrow x & y' in the carrier of (CompactSublatt L) ) by A4, Def1, WAYBEL_0:17;
hence y in (downarrow x) /\ the carrier of (CompactSublatt L) by A4, XBOOLE_0:def 4; :: thesis: verum

end;

then compactbelow x c= (downarrow x) /\ the carrier of (CompactSublatt L) by TARSKI:def 3;
hence compactbelow x = (downarrow x) /\ the carrier of (CompactSublatt L) by A3, XBOOLE_0:def 10; :: thesis: verum