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 )
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 ; :: thesis: verum