let C1, C2 be Convergence-Class of L; ( ( for N being net of L st N in NetUniv L holds
for x being Element of L holds
( [N,x] in C1 iff for M being subnet of N holds x = lim_inf M ) ) & ( for N being net of L st N in NetUniv L holds
for x being Element of L holds
( [N,x] in C2 iff for M being subnet of N holds x = lim_inf M ) ) implies C1 = C2 )
assume that
A4:
for N being net of L st N in NetUniv L holds
for x being Element of L holds
( [N,x] in C1 iff for M being subnet of N holds x = lim_inf M )
and
A5:
for N being net of L st N in NetUniv L holds
for x being Element of L holds
( [N,x] in C2 iff for M being subnet of N holds x = lim_inf M )
; C1 = C2
let Ns, xs be object ; RELAT_1:def 2 ( ( not [Ns,xs] in C1 or [Ns,xs] in C2 ) & ( not [Ns,xs] in C2 or [Ns,xs] in C1 ) )
A6:
C1 c= [:(NetUniv L), the carrier of L:]
by YELLOW_6:def 18;
thus
( [Ns,xs] in C1 implies [Ns,xs] in C2 )
( not [Ns,xs] in C2 or [Ns,xs] in C1 )proof
assume A7:
[Ns,xs] in C1
;
[Ns,xs] in C2
then reconsider x =
xs as
Element of
L by A6, ZFMISC_1:87;
Ns in NetUniv L
by A6, A7, ZFMISC_1:87;
then consider N being
strict net of
L such that A8:
N = Ns
and
the
carrier of
N in the_universe_of the
carrier of
L
by YELLOW_6:def 11;
A9:
N in NetUniv L
by A6, A7, A8, ZFMISC_1:87;
then
for
M being
subnet of
N holds
x = lim_inf M
by A4, A7, A8;
hence
[Ns,xs] in C2
by A5, A8, A9;
verum
end;
assume A10:
[Ns,xs] in C2
; [Ns,xs] in C1
A11:
C2 c= [:(NetUniv L), the carrier of L:]
by YELLOW_6:def 18;
then reconsider x = xs as Element of L by A10, ZFMISC_1:87;
Ns in NetUniv L
by A11, A10, ZFMISC_1:87;
then consider N being strict net of L such that
A12:
N = Ns
and
the carrier of N in the_universe_of the carrier of L
by YELLOW_6:def 11;
A13:
N in NetUniv L
by A11, A10, A12, ZFMISC_1:87;
then
for M being subnet of N holds x = lim_inf M
by A5, A10, A12;
hence
[Ns,xs] in C1
by A4, A12, A13; verum