let L be lower-bounded continuous Scott TopLattice; :: thesis: for x being Element of L holds wayabove x is open

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

set W = wayabove x;

wayabove x is inaccessible

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

set W = wayabove x;

wayabove x is inaccessible

proof

hence
wayabove x is open
by WAYBEL11:def 4; :: thesis: verum
let D be non empty directed Subset of L; :: according to WAYBEL11:def 1 :: thesis: ( not "\/" (D,L) in wayabove x or not D misses wayabove x )

assume sup D in wayabove x ; :: thesis: not D misses wayabove x

then x << sup D by WAYBEL_3:8;

then consider d being Element of L such that

A1: d in D and

A2: x << d by WAYBEL_4:53;

d in wayabove x by A2;

hence not D misses wayabove x by A1, XBOOLE_0:3; :: thesis: verum

end;assume sup D in wayabove x ; :: thesis: not D misses wayabove x

then x << sup D by WAYBEL_3:8;

then consider d being Element of L such that

A1: d in D and

A2: x << d by WAYBEL_4:53;

d in wayabove x by A2;

hence not D misses wayabove x by A1, XBOOLE_0:3; :: thesis: verum