defpred S₁[ object , object ] means ex N being net of T ex p being Point of T st
( N = $1 & p = $2 & p in Lim N );
consider R being Relation of (NetUniv T), the carrier of T such that
A1: for x, y being object 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 Def18;
take R ; :: thesis: for N being net of T
for p being Point of T holds
( [N,p] in R iff ( N in NetUniv T & p in Lim N ) )
let N be net of T; :: thesis: for p being Point of T holds
( [N,p] in R iff ( N in NetUniv T & p in Lim N ) )
let p be Point of T; :: 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 N9 being net of T ex p9 being Point of T st
( N9 = N & p9 = p & p9 in Lim N9 ) 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