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;
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 )
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;
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] and
a in f by A3;
reconsider f = f as a_neighborhood of x by A2, Th2;
A5: i `2 = f by A4;
f meets A by A1, CONNSP_2:27;
then consider b being object such that
A6: b in f and
A7: b in A by XBOOLE_0:3;
reconsider b = b as Element of T by A6;
[b,f] in the carrier of (a_net F) by A3, A6;
then reconsider j = [b,f] as Element of (a_net F) ;
take j ; :: thesis: ( i <= j & (a_net F) . j in A )
A8: j `1 = b ;
j `2 = f ;
hence ( i <= j & (a_net F) . j in A ) by A7, A5, A8, Def4; :: thesis: verum