let T be non empty TopSpace; :: thesis: ( T is locally-compact implies for D being countable Subset-Family of T st not D is empty & D is dense & D is open holds
for O being non empty Subset of T st O is open holds
ex A being irreducible Subset of T st
for V being Subset of T st V in D holds
A /\ O meets V )
assume T is locally-compact ; :: thesis: for D being countable Subset-Family of T st not D is empty & D is dense & D is open holds
for O being non empty Subset of T st O is open holds
ex A being irreducible Subset of T st
for V being Subset of T st V in D holds
A /\ O meets V
then reconsider L = InclPoset the topology of T as bounded continuous LATTICE by WAYBEL_3:42;
A1: the carrier of L = the topology of T by YELLOW_1:1;
let D be countable Subset-Family of T; :: thesis: ( not D is empty & D is dense & D is open implies for O being non empty Subset of T st O is open holds
ex A being irreducible Subset of T st
for V being Subset of T st V in D holds
A /\ O meets V )
assume A2: ( not D is empty & D is dense & D is open ) ; :: thesis: for O being non empty Subset of T st O is open holds
ex A being irreducible Subset of T st
for V being Subset of T st V in D holds
A /\ O meets V
consider I being object such that
A3: I in D by A2;
reconsider I = I as Subset of T by A3;
I is open by A2, A3;
then reconsider i = I as Element of L by A1;
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

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in { d where d is Element of L : ex d1 being Subset of T st
( d1 in D & d1 = d & d is dense ) } or q in the carrier of L )
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: q in the carrier of L
then ex d being Element of L st
( q = d & ex d1 being Subset of T st
( d1 in D & d1 = d & d is dense ) ) ;
hence q in the carrier of L ; :: thesis: verum

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 ;
A4: D1 c= D

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in D1 or q in D )
assume q in D1 ; :: thesis: q in D
then ex d being Element of L st
( q = d & ex d1 being Subset of T st
( d1 in D & d1 = d & d is dense ) ) ;
hence q in D ; :: thesis: verum

end;

A5: D1 is dense

proof

let q be Element of L; :: according to WAYBEL12:def 5 :: thesis: ( q in D1 implies q is dense )
assume q in D1 ; :: thesis: q is dense
then ex d being Element of L st
( q = d & ex d1 being Subset of T st
( d1 in D & d1 = d & d is dense ) ) ;
hence q is dense ; :: thesis: verum

end;

let O be non empty Subset of T; :: thesis: ( O is open implies ex A being irreducible Subset of T st
for V being Subset of T st V in D holds
A /\ O meets V )
assume A6: O is open ; :: thesis: ex A being irreducible Subset of T st
for V being Subset of T st V in D holds
A /\ O meets V
reconsider u = O as Element of L by A6, A1;
( I is open & I is dense ) by A2, A3;
then I is everywhere_dense by TOPS_3:36;
then i is dense by Th42;
then ( u <> Bottom L & i in D1 ) by A3, PRE_TOPC:1, YELLOW_1:13;
then consider p being irreducible Element of L such that
A7: p <> Top L and
A8: not p in uparrow ({u} "/\" D1) by A4, A5, Th39;
p in the topology of T by A1;
then reconsider P = p as Subset of T ;
reconsider A = P ` as irreducible Subset of T by A7, Th41;
take A ; :: thesis: for V being Subset of T st V in D holds
A /\ O meets V
let V be Subset of T; :: thesis: ( V in D implies A /\ O meets V )
assume A9: V in D ; :: thesis: A /\ O meets V
then A10: V is open by A2;
then reconsider v = V as Element of L by A1;
A11: for d1 being Element of L st d1 in D1 holds
not u "/\" d1 <= p

proof

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

end;

V is dense by A2, A9;
then V is everywhere_dense by A10, TOPS_3:36;
then v is dense by Th42;
then v in D1 by A9;
then not u "/\" v <= p by A11;
then A13: not u "/\" v c= p by YELLOW_1:3;
O /\ V is open by A6, A10;
then u /\ v in the topology of T ;
then not O /\ V c= p by A13, YELLOW_1:9;
then consider x being object such that
A14: x in O /\ V and
A15: not x in A ` ;
reconsider x = x as Element of T by A14;
x in A by A15, XBOOLE_0:def 5;
then (O /\ V) /\ A <> {} by A14, XBOOLE_0:def 4;
hence (A /\ O) /\ V <> {} by XBOOLE_1:16; :: according to XBOOLE_0:def 7 :: thesis: verum