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

now

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;

hence [#] L is Open by Def1; :: thesis: verum