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)

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

(waybelow x) /\ the carrier of (CompactSublatt L) c= compactbelow x
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;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

proof

hence
compactbelow x = (waybelow x) /\ the carrier of (CompactSublatt L)
by A1; :: thesis: verum
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;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