let T be non empty TopSpace; :: thesis:
assume T is locally-compact ; :: thesis:
then reconsider L = InclPoset the topology of T as bounded continuous LATTICE by WAYBEL_3:43;
let D be countable Subset-Family of T; :: thesis:
assume A1: ( not D is empty & D is dense & D is open ) ; :: thesis:
let O be non empty Subset of T; :: thesis:
assume A2: O is open ; :: thesis:
A3: the carrier of L = the topology of T by YELLOW_1:1;
then reconsider u = O as Element of L by A2, PRE_TOPC:def 5;
A4: u <> Bottom L by PRE_TOPC:5, YELLOW_1:13;
set D1 = { d where d is Element of L : ex d1 being Subset of T st
( d1 in D & d1 = d & d is dense ) } ;
{ d where d is Element of L : ex d1 being Subset of T st
( d1 in D & d1 = d & d is dense ) } c= the carrier of L

let q be set ; :: according to TARSKI:def 3 :: thesis:
assume q in { d where d is Element of L : ex d1 being Subset of T st
( d1 in D & d1 = d & d is dense ) } ; :: thesis:
then consider d being Element of L such that
A5: q = d and
ex d1 being Subset of T st
( d1 in D & d1 = d & d is dense ) ;
thus q in the carrier of L by A5; :: thesis:

end;

then reconsider D1 = { d where d is Element of L : ex d1 being Subset of T st
( d1 in D & d1 = d & d is dense ) } as Subset of L ;
D1 c= D

let q be set ; :: according to TARSKI:def 3 :: thesis:
assume q in D1 ; :: thesis:
then consider d being Element of L such that
A6: ( q = d & ex d1 being Subset of T st
( d1 in D & d1 = d & d is dense ) ) ;
thus q in D by A6; :: thesis:

end;

then A7: D1 is countable ;
A8: D1 is dense

let q be Element of L; :: according to WAYBEL12:def 5 :: thesis:
assume q in D1 ; :: thesis:
then consider d being Element of L such that
A9: ( q = d & ex d1 being Subset of T st
( d1 in D & d1 = d & d is dense ) ) ;
thus q is dense by A9; :: thesis:

end;

consider I being set such that
A10: I in D by A1, XBOOLE_0:def 1;
reconsider I = I as Subset of T by A10;
I is open by A1, A10, TOPS_2:def 1;
then reconsider i = I as Element of L by A3, PRE_TOPC:def 5;
( I is open & I is dense ) by A1, A10, Def2, TOPS_2:def 1;
then I is everywhere_dense by TOPS_3:36;
then i is dense by Th46;
then i in D1 by A10;
then consider p being irreducible Element of L such that
A11: p <> Top L and
A12: not p in uparrow ({u} "/\" D1) by A4, A7, A8, Th43;
p in the topology of T by A3;
then reconsider P = p as Subset of T ;
reconsider A = P ` as irreducible Subset of T by A11, Th45;
take A ; :: thesis:
let V be Subset of T; :: thesis:
assume A13: V in D ; :: thesis:
then A14: V is dense by A1, Def2;
A15: for d1 being Element of L st d1 in D1 holds
not u "/\" d1 <= p

let d1 be Element of L; :: thesis:
assume A16: d1 in D1 ; :: thesis:
u in {u} by TARSKI:def 1;
then u "/\" d1 in {u} "/\" D1 by A16;
hence not u "/\" d1 <= p by A12, WAYBEL_0:def 16; :: thesis:

end;

A17: V is open by A1, A13, TOPS_2:def 1;
then reconsider v = V as Element of L by A3, PRE_TOPC:def 5;
O /\ V is open by A2, A17, TOPS_1:38;
then A18: u /\ v in the topology of T by PRE_TOPC:def 5;
V is everywhere_dense by A14, A17, TOPS_3:36;
then v is dense by Th46;
then v in D1 by A13;
then not u "/\" v <= p by A15;
then not u "/\" v c= p by YELLOW_1:3;
then not O /\ V c= p by A18, YELLOW_1:9;
then consider x being set such that
A19: x in O /\ V and
A20: not x in A ` by TARSKI:def 3;
reconsider x = x as Element of T by A19;
x in A by A20, XBOOLE_0:def 5;
then (O /\ V) /\ A <> {} by A19, XBOOLE_0:def 4;
hence (A /\ O) /\ V <> {} by XBOOLE_1:16; :: according to XBOOLE_0:def 7 :: thesis: