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

let y be object ; :: 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 y9 = y as Element of L ;
y in downarrow x by A1, XBOOLE_0:def 4;
then A2: y9 <= x by WAYBEL_0:17;
y in the carrier of (CompactSublatt L) by A1, XBOOLE_0:def 4;
then y9 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 ;

now :: thesis: for y being object st y in compactbelow x holds
y in (downarrow x) /\ the carrier of (CompactSublatt L)

let y be object ; :: 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 y9 being Element of L such that
A4: y9 = y and
A5: ( y9 <= x & y9 is compact ) ;
( y9 in downarrow x & y9 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) ;
hence compactbelow x = (downarrow x) /\ the carrier of (CompactSublatt L) by A3, XBOOLE_0:def 10; :: thesis: verum