let S be non empty 1-sorted ; :: thesis: for C being Convergence-Class of S holds C c= Convergence (ConvergenceSpace C)
let C be Convergence-Class of S; :: thesis: C c= Convergence (ConvergenceSpace C)
set T = ConvergenceSpace C;
let x be set ; :: according to RELAT_1:def 3 :: thesis: for b₁ being set holds
( not [x,b₁] in C or [x,b₁] in Convergence (ConvergenceSpace C) )
let y be set ; :: thesis: ( not [x,y] in C or [x,y] in Convergence (ConvergenceSpace C) )
A1: C c= [:(NetUniv S),the carrier of S:] by Def21;
A2: the carrier of S = the carrier of (ConvergenceSpace C) by Def27;
assume A3: [x,y] in C ; :: thesis: [x,y] in Convergence (ConvergenceSpace C)
then consider M being Element of NetUniv S, p being Element of S such that
A4: [x,y] = [M,p] by A1, DOMAIN_1:9;
A5: M in NetUniv S ;
ex N being strict net of S st
( N = M & the carrier of N in the_universe_of the carrier of S ) by Def14;
then reconsider M = M as net of S ;
reconsider N = M as net of ConvergenceSpace C by Def27;
A6: N in NetUniv (ConvergenceSpace C) by A2, A5, Lm7;
reconsider q = p as Point of (ConvergenceSpace C) by Def27;
A7: the topology of (ConvergenceSpace C) = { V where V is Subset of S : for p being Element of S st p in V holds
for N being net of S st [N,p] in C holds
N is_eventually_in V } by Def27;

now

let V be a_neighborhood of q; :: thesis: N is_eventually_in V
A8: Int V c= V by TOPS_1:44;
A9: p in Int V by CONNSP_2:def 1;
Int V is open by TOPS_1:51;
then Int V in the topology of (ConvergenceSpace C) by PRE_TOPC:def 5;
then ex W being Subset of S st
( W = Int V & ( for p being Element of S st p in W holds
for N being net of S st [N,p] in C holds
N is_eventually_in W ) ) by A7;
then M is_eventually_in Int V by A3, A4, A9;
then consider ii being Element of M such that
A10: for j being Element of M st ii <= j holds
M . j in Int V by WAYBEL_0:def 11;
reconsider i = ii as Element of N ;

now

let j be Element of N; :: thesis: ( i <= j implies N . j in Int V )
assume A11: i <= j ; :: thesis: N . j in Int V
reconsider jj = j as Element of M ;
M . jj = N . j ;
hence N . j in Int V by A10, A11; :: thesis: verum

end;

then N is_eventually_in Int V by WAYBEL_0:def 11;
hence N is_eventually_in V by A8, WAYBEL_0:8; :: thesis: verum

end;

then p in Lim N by Def18;
hence [x,y] in Convergence (ConvergenceSpace C) by A4, A6, Def22; :: thesis: verum