let C1, C2 be Convergence-Class of L; :: thesis: ( ( 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
A7:
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
A8:
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 )
; :: thesis: C1 = C2
A9:
C1 c= [:(NetUniv L),the carrier of L:]
by YELLOW_6:def 21;
A10:
C2 c= [:(NetUniv L),the carrier of L:]
by YELLOW_6:def 21;
let Ns, xs be set ; :: according to RELAT_1:def 2 :: thesis: ( ( not [Ns,xs] in C1 or [Ns,xs] in C2 ) & ( not [Ns,xs] in C2 or [Ns,xs] in C1 ) )
thus
( [Ns,xs] in C1 implies [Ns,xs] in C2 )
:: thesis: ( not [Ns,xs] in C2 or [Ns,xs] in C1 )proof
assume A11:
[Ns,xs] in C1
;
:: thesis: [Ns,xs] in C2
then
Ns in NetUniv L
by A9, ZFMISC_1:106;
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 14;
A13:
N in NetUniv L
by A9, A11, A12, ZFMISC_1:106;
reconsider x =
xs as
Element of
L by A9, A11, ZFMISC_1:106;
for
M being
subnet of
N holds
x = lim_inf M
by A7, A11, A12, A13;
hence
[Ns,xs] in C2
by A8, A12, A13;
:: thesis: verum
end;
assume A14:
[Ns,xs] in C2
; :: thesis: [Ns,xs] in C1
then
Ns in NetUniv L
by A10, ZFMISC_1:106;
then consider N being strict net of L such that
A15:
N = Ns
and
the carrier of N in the_universe_of the carrier of L
by YELLOW_6:def 14;
A16:
N in NetUniv L
by A10, A14, A15, ZFMISC_1:106;
reconsider x = xs as Element of L by A10, A14, ZFMISC_1:106;
for M being subnet of N holds x = lim_inf M
by A8, A14, A15, A16;
hence
[Ns,xs] in C1
by A7, A15, A16; :: thesis: verum