let T be non empty TopSpace; :: thesis: for x being Point of T
for A being Subset of T st x in Cl A holds
for F being proper Filter of (BoolePoset ([#] T)) st F = NeighborhoodSystem x holds
a_net F is_often_in A
let x be Point of T; :: thesis: for A being Subset of T st x in Cl A holds
for F being proper Filter of (BoolePoset ([#] T)) st F = NeighborhoodSystem x holds
a_net F is_often_in A
let A be Subset of T; :: thesis: ( x in Cl A implies for F being proper Filter of (BoolePoset ([#] T)) st F = NeighborhoodSystem x holds
a_net F is_often_in A )
assume A1: x in Cl A ; :: thesis: for F being proper Filter of (BoolePoset ([#] T)) st F = NeighborhoodSystem x holds
a_net F is_often_in A
let F be proper Filter of (BoolePoset ([#] T)); :: thesis: ( F = NeighborhoodSystem x implies a_net F is_often_in A )
assume A2: F = NeighborhoodSystem x ; :: thesis: a_net F is_often_in A
set N = a_net F;
A3: the carrier of (a_net F) = { [a,f] where a is Element of T, f is Element of F : a in f } by Def4;
let i be Element of (a_net F); :: according to WAYBEL_0:def 12 :: thesis: ex b₁ being Element of the carrier of (a_net F) st
( i <= b₁ & (a_net F) . b₁ in A )
i in the carrier of (a_net F) ;
then consider a being Element of T, f being Element of F such that
A4: ( i = [a,f] & a in f ) by A3;
reconsider f = f as a_neighborhood of x by A2, Th3;
f meets A by A1, CONNSP_2:34;
then consider b being set such that
A5: ( b in f & b in A ) by XBOOLE_0:3;
reconsider b = b as Element of T by A5;
[b,f] in the carrier of (a_net F) by A3, A5;
then reconsider j = [b,f] as Element of (a_net F) ;
take j ; :: thesis: ( i <= j & (a_net F) . j in A )
( i `2 = f & j `2 = f & j `1 = b ) by A4, MCART_1:7;
hence ( i <= j & (a_net F) . j in A ) by A5, Def4; :: thesis: verum