defpred S₁[ set , Element of R] means ex N being strict net of R st
( N = $1 & $2 is_S-limit_of N );
consider C being Relation of (NetUniv R), the carrier of R such that
A1: for x being Element of NetUniv R
for y being Element of R holds
( [x,y] in C iff S₁[x,y] ) from RELSET_1:sch 2();
reconsider C = C as Convergence-Class of R by YELLOW_6:def 18;
take C ; :: thesis: for N being strict net of R st N in NetUniv R holds
for p being Element of R holds
( [N,p] in C iff p is_S-limit_of N )
let N be strict net of R; :: thesis: ( N in NetUniv R implies for p being Element of R holds
( [N,p] in C iff p is_S-limit_of N ) )
assume A2: N in NetUniv R ; :: thesis: for p being Element of R holds
( [N,p] in C iff p is_S-limit_of N )
let p be Element of R; :: thesis: ( [N,p] in C iff p is_S-limit_of N )

hereby :: thesis: ( p is_S-limit_of N implies [N,p] in C )

assume [N,p] in C ; :: thesis: p is_S-limit_of N
then ex M being strict net of R st
( M = N & p is_S-limit_of M ) by A1, A2;
hence p is_S-limit_of N ; :: thesis: verum

end;

thus ( p is_S-limit_of N implies [N,p] in C ) by A1, A2; :: thesis: verum