let L be lower-bounded continuous LATTICE; :: thesis: for x being Element of holds wayabove x is Open
let x be Element of ; :: thesis: wayabove x is Open
for l being Element of st l in wayabove x holds
ex y being Element of st
( y in wayabove x & y << l )

proof

let l be Element of ; :: thesis: ( l in wayabove x implies ex y being Element of st
( y in wayabove x & y << l ) )
assume l in wayabove x ; :: thesis: ex y being Element of st
( y in wayabove x & y << l )
then x << l by WAYBEL_3:8;
then consider y being Element of such that
A1: ( x << y & y << l ) by WAYBEL_4:53;
take y ; :: thesis: ( y in wayabove x & y << l )
thus ( y in wayabove x & y << l ) by A1, WAYBEL_3:8; :: thesis: verum

end;

hence wayabove x is Open by Def1; :: thesis: verum