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 reconsider y' = y as Element of L ;
y in downarrow x by A1, XBOOLE_0:def 4;
then A2: y' <= x by WAYBEL_0:17;
y in the carrier of (CompactSublatt L) by A1, XBOOLE_0:def 4;
then y' is compact by Def1;
hence y in compactbelow x by A2; :: 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 and
A5: ( y' <= x & y' is compact ) ;
( y' in downarrow x & y' in the carrier of (CompactSublatt L) ) by A5, 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