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

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