let L be continuous Semilattice; :: thesis: for x being Element of L holds

( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds

waybelow x c= I ) )

let x be Element of L; :: thesis: ( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds

waybelow x c= I ) )

thus waybelow x is Ideal of L ; :: thesis: ( x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds

waybelow x c= I ) )

thus x <= sup (waybelow x) by WAYBEL_3:def 5; :: thesis: for I being Ideal of L st x <= sup I holds

waybelow x c= I

thus for I being Ideal of L st x <= sup I holds

waybelow x c= I :: thesis: verum

( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds

waybelow x c= I ) )

let x be Element of L; :: thesis: ( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds

waybelow x c= I ) )

thus waybelow x is Ideal of L ; :: thesis: ( x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds

waybelow x c= I ) )

thus x <= sup (waybelow x) by WAYBEL_3:def 5; :: thesis: for I being Ideal of L st x <= sup I holds

waybelow x c= I

thus for I being Ideal of L st x <= sup I holds

waybelow x c= I :: thesis: verum

proof

let I be Ideal of L; :: thesis: ( x <= sup I implies waybelow x c= I )

assume A1: x <= sup I ; :: thesis: waybelow x c= I

waybelow x c= I

end;assume A1: x <= sup I ; :: thesis: waybelow x c= I

waybelow x c= I

proof

hence
waybelow x c= I
; :: thesis: verum
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in waybelow x or y in I )

assume y in waybelow x ; :: thesis: y in I

then y in { y9 where y9 is Element of L : y9 << x } by WAYBEL_3:def 3;

then ex y9 being Element of L st

( y = y9 & y9 << x ) ;

hence y in I by A1, WAYBEL_3:20; :: thesis: verum

end;assume y in waybelow x ; :: thesis: y in I

then y in { y9 where y9 is Element of L : y9 << x } by WAYBEL_3:def 3;

then ex y9 being Element of L st

( y = y9 & y9 << x ) ;

hence y in I by A1, WAYBEL_3:20; :: thesis: verum