let T be complete Scott TopLattice; :: thesis: for S being upper Subset of T st S is Open holds
S is open
let S be upper Subset of T; :: thesis: ( S is Open implies S is open )
assume A1: for x being Element of T st x in S holds
ex y being Element of T st
( y in S & y << x ) ; :: according to WAYBEL_6:def 1 :: thesis: S is open
S is inaccessible
proof
let D be non empty directed Subset of T; :: according to WAYBEL11:def 1 :: thesis: ( sup D in S implies D meets S )
assume sup D in S ; :: thesis: D meets S
then consider y being Element of T such that
A2: y in S and
A3: y << sup D by A1;
consider d being Element of T such that
A4: d in D and
A5: y <= d by A3;
d in S by A2, A5, WAYBEL_0:def 20;
hence D meets S by A4, XBOOLE_0:3; :: thesis: verum
end;
hence S is open by Def4; :: thesis: verum