take
[#] L
; :: thesis: [#] L is Open

now :: thesis: for x being Element of L st x in [#] L holds

ex y being Element of L st

( y in [#] L & y << x )

hence
[#] L is Open
; :: thesis: verumex y being Element of L st

( y in [#] L & y << x )

let x be Element of L; :: thesis: ( x in [#] L implies ex y being Element of L st

( y in [#] L & y << x ) )

assume x in [#] L ; :: thesis: ex y being Element of L st

( y in [#] L & y << x )

Bottom L << x by WAYBEL_3:4;

hence ex y being Element of L st

( y in [#] L & y << x ) ; :: thesis: verum

end;( y in [#] L & y << x ) )

assume x in [#] L ; :: thesis: ex y being Element of L st

( y in [#] L & y << x )

Bottom L << x by WAYBEL_3:4;

hence ex y being Element of L st

( y in [#] L & y << x ) ; :: thesis: verum