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 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 Def24;
then A2: ( 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 ) ) ) ;
the carrier of (ConvergenceSpace C) = the carrier of T by Def24;
then ( ( 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;
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 A2; :: thesis: verum