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

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 ) ; :: thesis: C1 = C2

let Ns, xs be object ; :: 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 ) )

A6: C1 c= [:(NetUniv L), the carrier of L:] by YELLOW_6:def 18;

thus ( [Ns,xs] in C1 implies [Ns,xs] in C2 ) :: thesis: ( not [Ns,xs] in C2 or [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; :: thesis: verum

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 ) ; :: thesis: C1 = C2

let Ns, xs be object ; :: 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 ) )

A6: C1 c= [:(NetUniv L), the carrier of L:] by YELLOW_6:def 18;

thus ( [Ns,xs] in C1 implies [Ns,xs] in C2 ) :: thesis: ( not [Ns,xs] in C2 or [Ns,xs] in C1 )

proof

assume A10:
[Ns,xs] in C2
; :: thesis: [Ns,xs] in C1
assume A7:
[Ns,xs] in C1
; :: thesis: [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; :: thesis: verum

end;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; :: thesis: verum

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; :: thesis: verum