defpred S₁[ set , Element of ] means ex N being strict net of strict st
( N = $1 & $2 is_S-limit_of N );
consider C being Relation of , such that
A1: for x being Element of NetUniv R
for y being Element of 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 21;
take C ; :: thesis: for N being strict net of strict st N in NetUniv R holds
for p being Element of holds
( [N,p] in C iff p is_S-limit_of N )
let N be strict net of strict ; :: thesis: ( N in NetUniv R implies for p being Element of holds
( [N,p] in C iff p is_S-limit_of N ) )
assume A2: N in NetUniv R ; :: thesis: for p being Element of holds
( [N,p] in C iff p is_S-limit_of N )
let p be Element of ; :: 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 strict 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