let L be complete continuous Scott TopLattice; :: thesis: for p being Element of L
for S being Subset of L st S is open & p in S holds
ex q being Element of L st
( q << p & q in S )
let p be Element of L; :: thesis: for S being Subset of L st S is open & p in S holds
ex q being Element of L st
( q << p & q in S )
let S be Subset of L; :: thesis: ( S is open & p in S implies ex q being Element of L st
( q << p & q in S ) )
assume that
A1: S is open and
A2: p in S ; :: thesis: ex q being Element of L st
( q << p & q in S )
A3: S is inaccessible by A1, Def4;
sup (waybelow p) = p by WAYBEL_3:def 5;
then waybelow p meets S by A2, A3;
then (waybelow p) /\ S <> {} ;
then consider u being Element of L such that
A4: u in (waybelow p) /\ S by SUBSET_1:4;
reconsider u = u as Element of L ;
take u ; :: thesis: ( u << p & u in S )
u in waybelow p by A4, XBOOLE_0:def 4;
hence u << p by WAYBEL_3:7; :: thesis: u in S
thus u in S by A4, XBOOLE_0:def 4; :: thesis: verum