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_{1} being Element of the carrier of (a_net F) st

( i <= b_{1} & (a_net F) . b_{1} 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

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

( i <= b

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