let L be lower-bounded continuous LATTICE; :: thesis: for x being Element of L holds wayabove x is Open

let x be Element of L; :: thesis: wayabove x is Open

for l being Element of L st l in wayabove x holds

ex y being Element of L st

( y in wayabove x & y << l )

let x be Element of L; :: thesis: wayabove x is Open

for l being Element of L st l in wayabove x holds

ex y being Element of L st

( y in wayabove x & y << l )

proof

hence
wayabove x is Open
; :: thesis: verum
let l be Element of L; :: thesis: ( l in wayabove x implies ex y being Element of L st

( y in wayabove x & y << l ) )

assume l in wayabove x ; :: thesis: ex y being Element of L st

( y in wayabove x & y << l )

then x << l by WAYBEL_3:8;

then consider y being Element of L such that

A1: ( x << y & y << l ) by WAYBEL_4:52;

take y ; :: thesis: ( y in wayabove x & y << l )

thus ( y in wayabove x & y << l ) by A1, WAYBEL_3:8; :: thesis: verum

end;( y in wayabove x & y << l ) )

assume l in wayabove x ; :: thesis: ex y being Element of L st

( y in wayabove x & y << l )

then x << l by WAYBEL_3:8;

then consider y being Element of L such that

A1: ( x << y & y << l ) by WAYBEL_4:52;

take y ; :: thesis: ( y in wayabove x & y << l )

thus ( y in wayabove x & y << l ) by A1, WAYBEL_3:8; :: thesis: verum