let T be non empty TopSpace; ( 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
; 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; ( 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 )
; 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
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
A5:
D1 is dense
let O be non empty Subset of T; ( 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
; 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
; for V being Subset of T st V in D holds
A /\ O meets V
let V be Subset of T; ( V in D implies A /\ O meets V )
assume A9:
V in D
; 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
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; XBOOLE_0:def 7 verum