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

( d1 in D & d1 = d & d is dense ) } as Subset of L ;

A4: D1 c= D

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

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

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

then reconsider D1 = { d where d is Element of L : ex d1 being Subset of T st
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;( 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

( d1 in D & d1 = d & d is dense ) } as Subset of L ;

A4: D1 c= D

proof

A5:
D1 is dense
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;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

proof

let O be non empty Subset of T; :: thesis: ( O is open implies ex A being irreducible Subset of T st
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;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

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

V is dense
by A2, A9;
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;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

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