let L be 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, WAYBEL11:def 4;
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 object such that
A4: u in (waybelow p) /\ S by XBOOLE_0:def 1;
A5: u in waybelow p by A4, XBOOLE_0:def 4;
reconsider u = u as Element of L by A4;
take u ; :: thesis: ( u << p & u in S )
thus u << p by A5, WAYBEL_3:7; :: thesis: u in S
thus u in S by A4, XBOOLE_0:def 4; :: thesis: verum