let T be non empty 1-sorted ; :: thesis: for C being topological Convergence-Class of T
for S being Subset of (ConvergenceSpace C) holds
( S is open iff for p being Element of T st p in S holds
for N being net of T st [N,p] in C holds
N is_eventually_in S )
let C be topological Convergence-Class of T; :: thesis: for S being Subset of (ConvergenceSpace C) holds
( S is open iff for p being Element of T st p in S holds
for N being net of T st [N,p] in C holds
N is_eventually_in S )
let S be Subset of (ConvergenceSpace C); :: thesis: ( S is open iff for p being Element of T st p in S holds
for N being net of T st [N,p] in C holds
N is_eventually_in S )
A1: the carrier of (ConvergenceSpace C) = the carrier of T by Def27;
A2: the topology of (ConvergenceSpace C) = { V where V is Subset of T : for p being Element of T st p in V holds
for N being net of T st [N,p] in C holds
N is_eventually_in V } by Def27;
then A3: ( ( for p being Element of T st p in S holds
for N being net of T st [N,p] in C holds
N is_eventually_in S ) implies S in the topology of (ConvergenceSpace C) ) by A1;
( S in the topology of (ConvergenceSpace C) implies ex V being Subset of T st
( S = V & ( for p being Element of T st p in V holds
for N being net of T st [N,p] in C holds
N is_eventually_in V ) ) ) by A2;
hence ( S is open iff for p being Element of T st p in S holds
for N being net of T st [N,p] in C holds
N is_eventually_in S ) by A3, PRE_TOPC:def 5; :: thesis: verum