let it1, it2 be Convergence-Class of R; :: thesis: ( ( for N being strict net of R st N in NetUniv R holds
for p being Element of R holds
( [N,p] in it1 iff p is_S-limit_of N ) ) & ( for N being strict net of R st N in NetUniv R holds
for p being Element of R holds
( [N,p] in it2 iff p is_S-limit_of N ) ) implies it1 = it2 )
assume that
A3: for N being strict net of R st N in NetUniv R holds
for p being Element of R holds
( [N,p] in it1 iff p is_S-limit_of N ) and
A4: for N being strict net of R st N in NetUniv R holds
for p being Element of R holds
( [N,p] in it2 iff p is_S-limit_of N ) ; :: thesis: it1 = it2
let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in it1 or [x,y] in it2 ) & ( not [x,y] in it2 or [x,y] in it1 ) )
A5: it1 c= [:(NetUniv R), the carrier of R:] by YELLOW_6:def 18;
A6: it2 c= [:(NetUniv R), the carrier of R:] by YELLOW_6:def 18;

hereby :: thesis: ( not [x,y] in it2 or [x,y] in it1 )

assume A7: [x,y] in it1 ; :: thesis: [x,y] in it2
then A8: x in NetUniv R by A5, ZFMISC_1:87;
then consider N being strict net of R such that
A9: N = x and
the carrier of N in the_universe_of the carrier of R by YELLOW_6:def 11;
reconsider p = y as Element of R by A5, A7, ZFMISC_1:87;
p is_S-limit_of N by A3, A7, A8, A9;
hence [x,y] in it2 by A4, A8, A9; :: thesis: verum

end;

assume A10: [x,y] in it2 ; :: thesis: [x,y] in it1
then A11: x in NetUniv R by A6, ZFMISC_1:87;
then consider N being strict net of R such that
A12: N = x and
the carrier of N in the_universe_of the carrier of R by YELLOW_6:def 11;
reconsider p = y as Element of R by A6, A10, ZFMISC_1:87;
p is_S-limit_of N by A4, A10, A11, A12;
hence [x,y] in it1 by A3, A11, A12; :: thesis: verum