let T1, T2 be non empty TopSpace; ( TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) implies Convergence T1 = Convergence T2 )
assume A1:
TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #)
; Convergence T1 = Convergence T2
A2:
Convergence T1 c= [:(NetUniv T1), the carrier of T1:]
by YELLOW_6:def 18;
A3:
Convergence T2 c= [:(NetUniv T2), the carrier of T2:]
by YELLOW_6:def 18;
let u1, u2 be object ; RELAT_1:def 2 ( ( not [u1,u2] in Convergence T1 or [u1,u2] in Convergence T2 ) & ( not [u1,u2] in Convergence T2 or [u1,u2] in Convergence T1 ) )
hereby ( not [u1,u2] in Convergence T2 or [u1,u2] in Convergence T1 )
assume A4:
[u1,u2] in Convergence T1
;
[u1,u2] in Convergence T2then consider N1 being
Element of
NetUniv T1,
p1 being
Point of
T1 such that A5:
[u1,u2] = [N1,p1]
by A2, DOMAIN_1:1;
A6:
N1 in NetUniv T1
;
ex
N being
strict net of
T1 st
(
N = N1 & the
carrier of
N in the_universe_of the
carrier of
T1 )
by YELLOW_6:def 11;
then reconsider N1 =
N1 as
net of
T1 ;
A7:
p1 in Lim N1
by A4, A5, YELLOW_6:def 19;
reconsider N2 =
N1 as
net of
T2 by A1;
reconsider p2 =
p1 as
Point of
T2 by A1;
A8:
N2 in NetUniv T2
by A1, A6, Lm5;
p2 in Lim N2
by A1, A7, Lm7;
hence
[u1,u2] in Convergence T2
by A5, A8, YELLOW_6:def 19;
verum
end;
assume A9:
[u1,u2] in Convergence T2
; [u1,u2] in Convergence T1
then consider N1 being Element of NetUniv T2, p1 being Point of T2 such that
A10:
[u1,u2] = [N1,p1]
by A3, DOMAIN_1:1;
A11:
N1 in NetUniv T2
;
ex N being strict net of T2 st
( N = N1 & the carrier of N in the_universe_of the carrier of T2 )
by YELLOW_6:def 11;
then reconsider N1 = N1 as net of T2 ;
A12:
p1 in Lim N1
by A9, A10, YELLOW_6:def 19;
reconsider N2 = N1 as net of T1 by A1;
reconsider p2 = p1 as Point of T1 by A1;
A13:
N2 in NetUniv T1
by A1, A11, Lm5;
p2 in Lim N2
by A1, A12, Lm7;
hence
[u1,u2] in Convergence T1
by A10, A13, YELLOW_6:def 19; verum