let it1, it2 be Convergence-Class of T; :: thesis: ( ( for N being net of T
for p being Point of T holds
( [N,p] in it1 iff ( N in NetUniv T & p in Lim N ) ) ) & ( for N being net of T
for p being Point of T holds
( [N,p] in it2 iff ( N in NetUniv T & p in Lim N ) ) ) implies it1 = it2 )
assume that
A3: for N being net of T
for p being Point of T holds
( [N,p] in it1 iff ( N in NetUniv T & p in Lim N ) ) and
A4: for N being net of T
for p being Point of T holds
( [N,p] in it2 iff ( N in NetUniv T & p in Lim N ) ) ; :: thesis: it1 = it2
A5: it1 c= [:(NetUniv T),the carrier of T:] by Def21;
A6: it2 c= [:(NetUniv T),the carrier of T:] by Def21;
let x be set ; :: according to RELAT_1:def 2 :: thesis: for b₁ being set holds
( ( not [x,b₁] in it1 or [x,b₁] in it2 ) & ( not [x,b₁] in it2 or [x,b₁] in it1 ) )
let y be set ; :: thesis: ( ( not [x,y] in it1 or [x,y] in it2 ) & ( not [x,y] in it2 or [x,y] in it1 ) )
thus ( [x,y] in it1 implies [x,y] in it2 ) :: thesis: ( not [x,y] in it2 or [x,y] in it1 )

proof

assume A7: [x,y] in it1 ; :: thesis: [x,y] in it2
then x in NetUniv T by A5, ZFMISC_1:106;
then consider N being strict net of T such that
A8: N = x and
the carrier of N in the_universe_of the carrier of T by Def14;
reconsider p = y as Point of T by A5, A7, ZFMISC_1:106;
[N,p] in it1 by A7, A8;
then ( N in NetUniv T & p in Lim N ) by A3;
hence [x,y] in it2 by A4, A8; :: thesis: verum

end;

assume A9: [x,y] in it2 ; :: thesis: [x,y] in it1
then x in NetUniv T by A6, ZFMISC_1:106;
then consider N being strict net of T such that
A10: N = x and
the carrier of N in the_universe_of the carrier of T by Def14;
reconsider p = y as Point of T by A6, A9, ZFMISC_1:106;
[N,p] in it2 by A9, A10;
then ( N in NetUniv T & p in Lim N ) by A4;
hence [x,y] in it1 by A3, A10; :: thesis: verum