defpred S₁[ set , set ] means ex N being net of ex p being Point of st
( N = $1 & p = $2 & p in Lim N );
consider R being Relation of , such that
A1: for x, y being set holds
( [x,y] in R iff ( x in NetUniv T & y in the carrier of T & S₁[x,y] ) ) from RELSET_1:sch 1();
reconsider R = R as Convergence-Class of T by Def21;
take R ; :: thesis: for N being net of
for p being Point of holds
( [N,p] in R iff ( N in NetUniv T & p in Lim N ) )
let N be net of ; :: thesis: for p being Point of holds
( [N,p] in R iff ( N in NetUniv T & p in Lim N ) )
let p be Point of ; :: thesis: ( [N,p] in R iff ( N in NetUniv T & p in Lim N ) )

hereby :: thesis: ( N in NetUniv T & p in Lim N implies [N,p] in R )

assume A2: [N,p] in R ; :: thesis: ( N in NetUniv T & p in Lim N )
hence N in NetUniv T by A1; :: thesis: p in Lim N
ex N' being net of ex p' being Point of st
( N' = N & p' = p & p' in Lim N' ) by A1, A2;
hence p in Lim N ; :: thesis: verum

end;

thus ( N in NetUniv T & p in Lim N implies [N,p] in R ) by A1; :: thesis: verum