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