let it1, it2 be Convergence-Class of T; ( ( 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 ) )
; it1 = it2
let x, y be object ; RELAT_1:def 2 ( ( not [x,y] in it1 or [x,y] in it2 ) & ( not [x,y] in it2 or [x,y] in it1 ) )
A5:
it1 c= [:(NetUniv T), the carrier of T:]
by Def18;
thus
( [x,y] in it1 implies [x,y] in it2 )
( not [x,y] in it2 or [x,y] in it1 )proof
assume A6:
[x,y] in it1
;
[x,y] in it2
then reconsider p =
y as
Point of
T by A5, ZFMISC_1:87;
x in NetUniv T
by A5, A6, ZFMISC_1:87;
then consider N being
strict net of
T such that A7:
N = x
and
the
carrier of
N in the_universe_of the
carrier of
T
by Def11;
[N,p] in it1
by A6, A7;
then A8:
N in NetUniv T
by A3;
p in Lim N
by A3, A6, A7;
hence
[x,y] in it2
by A4, A7, A8;
verum
end;
assume A9:
[x,y] in it2
; [x,y] in it1
A10:
it2 c= [:(NetUniv T), the carrier of T:]
by Def18;
then reconsider p = y as Point of T by A9, ZFMISC_1:87;
x in NetUniv T
by A10, A9, ZFMISC_1:87;
then consider N being strict net of T such that
A11:
N = x
and
the carrier of N in the_universe_of the carrier of T
by Def11;
[N,p] in it2
by A9, A11;
then A12:
N in NetUniv T
by A4;
p in Lim N
by A4, A9, A11;
hence
[x,y] in it1
by A3, A11, A12; verum