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 )
proof
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;
hence wayabove x is Open ; :: thesis: verum