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= [:(), 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 A7: [Ns,xs] in C1 ; :: thesis: [Ns,xs] in C2
then reconsider x = xs as Element of L by ;
Ns in NetUniv L by ;
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 ;
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;
assume A10: [Ns,xs] in C2 ; :: thesis: [Ns,xs] in C1
A11: C2 c= [:(), the carrier of L:] by YELLOW_6:def 18;
then reconsider x = xs as Element of L by ;
Ns in NetUniv L by ;
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 ;
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