let S be non empty 1-sorted ; :: thesis:
let C be Convergence-Class of S; :: thesis:
set T = ConvergenceSpace C;
let x, y be object ; :: according to RELAT_1:def 3 :: thesis:
assume A1: [x,y] in C ; :: thesis:
C c= [:(NetUniv S), the carrier of S:] by Def18;
then consider M being Element of NetUniv S, p being Element of S such that
A2: [x,y] = [M,p] by A1, DOMAIN_1:1;
reconsider q = p as Point of (ConvergenceSpace C) by Def24;
A3: ( the carrier of S = the carrier of (ConvergenceSpace C) & M in NetUniv S ) by Def24;
ex N being strict net of S st
( N = M & the carrier of N in the_universe_of the carrier of S ) by Def11;
then reconsider M = M as net of S ;
reconsider N = M as net of ConvergenceSpace C by Def24;
A4: 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 Def24;

now :: thesis:

let V be a_neighborhood of q; :: thesis:
Int V in the topology of (ConvergenceSpace C) by PRE_TOPC:def 2;
then ( p in Int V & 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 A4, CONNSP_2:def 1;
then M is_eventually_in Int V by A1, A2;
then consider ii being Element of M such that
A5: for j being Element of M st ii <= j holds
M . j in Int V ;
reconsider i = ii as Element of N ;

now :: thesis:

let j be Element of N; :: thesis:
assume A6: i <= j ; :: thesis:
reconsider jj = j as Element of M ;
M . jj = N . j ;
hence N . j in Int V by A5, A6; :: thesis:

end;

then ( Int V c= V & N is_eventually_in Int V ) by TOPS_1:16;
hence N is_eventually_in V by WAYBEL_0:8; :: thesis:

end;

then A7: p in Lim N by Def15;
N in NetUniv (ConvergenceSpace C) by A3, Lm7;
hence [x,y] in Convergence (ConvergenceSpace C) by A2, A7, Def19; :: thesis: