let L be non empty Poset; :: thesis: for x being Element of L holds compactbelow x = (waybelow x) /\ the carrier of (CompactSublatt L)
let x be Element of L; :: thesis: compactbelow x = (waybelow x) /\ the carrier of (CompactSublatt L)
A1: compactbelow x c= (waybelow x) /\ the carrier of (CompactSublatt L)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in compactbelow x or y in (waybelow x) /\ the carrier of (CompactSublatt L) )
assume A2: y in compactbelow x ; :: thesis: y in (waybelow x) /\ the carrier of (CompactSublatt L)
then reconsider y1 = y as Element of L ;
A3: y in (downarrow x) /\ the carrier of (CompactSublatt L) by A2, WAYBEL_8:5;
then y in downarrow x by XBOOLE_0:def 4;
then A4: y1 <= x by WAYBEL_0:17;
A5: y in the carrier of (CompactSublatt L) by A3, XBOOLE_0:def 4;
then y1 is compact by WAYBEL_8:def 1;
then y1 << y1 by WAYBEL_3:def 2;
then y1 << x by A4, WAYBEL_3:2;
then y1 in waybelow x by WAYBEL_3:7;
hence y in (waybelow x) /\ the carrier of (CompactSublatt L) by A5, XBOOLE_0:def 4; :: thesis: verum
end;
(waybelow x) /\ the carrier of (CompactSublatt L) c= compactbelow x
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (waybelow x) /\ the carrier of (CompactSublatt L) or y in compactbelow x )
assume A6: y in (waybelow x) /\ the carrier of (CompactSublatt L) ; :: thesis: y in compactbelow x
then reconsider y1 = y as Element of L ;
y in waybelow x by A6, XBOOLE_0:def 4;
then y1 << x by WAYBEL_3:7;
then y1 <= x by WAYBEL_3:1;
then A7: y in downarrow x by WAYBEL_0:17;
y in the carrier of (CompactSublatt L) by A6, XBOOLE_0:def 4;
then y in (downarrow x) /\ the carrier of (CompactSublatt L) by A7, XBOOLE_0:def 4;
hence y in compactbelow x by WAYBEL_8:5; :: thesis: verum
end;
hence compactbelow x = (waybelow x) /\ the carrier of (CompactSublatt L) by A1; :: thesis: verum