defpred S_{1}[ set , set ] means ex N being strict net of L st

( $1 = N & ( for M being subnet of N holds $2 = lim_inf M ) );

consider C being Relation of (NetUniv L), the carrier of L such that

A1: for N9 being Element of NetUniv L

for x being Element of L holds

( [N9,x] in C iff S_{1}[N9,x] )
from RELSET_1:sch 2();

reconsider C = C as Convergence-Class of L by YELLOW_6:def 18;

take C ; :: thesis: for N being net of L st N in NetUniv L holds

for x being Element of L holds

( [N,x] in C iff for M being subnet of N holds x = lim_inf M )

let N be net of L; :: thesis: ( N in NetUniv L implies for x being Element of L holds

( [N,x] in C iff for M being subnet of N holds x = lim_inf M ) )

assume N in NetUniv L ; :: thesis: for x being Element of L holds

( [N,x] in C iff for M being subnet of N holds x = lim_inf M )

then reconsider N1 = N as Element of NetUniv L ;

let x be Element of L; :: thesis: ( [N,x] in C iff for M being subnet of N holds x = lim_inf M )

thus ( [N,x] in C implies for M being subnet of N holds x = lim_inf M ) :: thesis: ( ( for M being subnet of N holds x = lim_inf M ) implies [N,x] in C )

( N2 = N1 & the carrier of N2 in the_universe_of the carrier of L ) by YELLOW_6:def 11;

assume for M being subnet of N holds x = lim_inf M ; :: thesis: [N,x] in C

hence [N,x] in C by A1, A3; :: thesis: verum

( $1 = N & ( for M being subnet of N holds $2 = lim_inf M ) );

consider C being Relation of (NetUniv L), the carrier of L such that

A1: for N9 being Element of NetUniv L

for x being Element of L holds

( [N9,x] in C iff S

reconsider C = C as Convergence-Class of L by YELLOW_6:def 18;

take C ; :: thesis: for N being net of L st N in NetUniv L holds

for x being Element of L holds

( [N,x] in C iff for M being subnet of N holds x = lim_inf M )

let N be net of L; :: thesis: ( N in NetUniv L implies for x being Element of L holds

( [N,x] in C iff for M being subnet of N holds x = lim_inf M ) )

assume N in NetUniv L ; :: thesis: for x being Element of L holds

( [N,x] in C iff for M being subnet of N holds x = lim_inf M )

then reconsider N1 = N as Element of NetUniv L ;

let x be Element of L; :: thesis: ( [N,x] in C iff for M being subnet of N holds x = lim_inf M )

thus ( [N,x] in C implies for M being subnet of N holds x = lim_inf M ) :: thesis: ( ( for M being subnet of N holds x = lim_inf M ) implies [N,x] in C )

proof

A3:
ex N2 being strict net of L st
assume A2:
[N,x] in C
; :: thesis: for M being subnet of N holds x = lim_inf M

let M be subnet of N; :: thesis: x = lim_inf M

ex N2 being strict net of L st

( N1 = N2 & ( for M being subnet of N2 holds x = lim_inf M ) ) by A1, A2;

hence x = lim_inf M ; :: thesis: verum

end;let M be subnet of N; :: thesis: x = lim_inf M

ex N2 being strict net of L st

( N1 = N2 & ( for M being subnet of N2 holds x = lim_inf M ) ) by A1, A2;

hence x = lim_inf M ; :: thesis: verum

( N2 = N1 & the carrier of N2 in the_universe_of the carrier of L ) by YELLOW_6:def 11;

assume for M being subnet of N holds x = lim_inf M ; :: thesis: [N,x] in C

hence [N,x] in C by A1, A3; :: thesis: verum