let L be complete 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
proof
let D be non empty directed Subset of L; :: according to WAYBEL11:def 1 :: thesis: ( sup D in wayabove x implies D meets wayabove x )
assume sup D in wayabove x ; :: thesis: D meets 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 D meets wayabove x by A1, XBOOLE_0:3; :: thesis: verum
end;
hence wayabove x is open by Def4; :: thesis: verum