defpred S₁[ 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₁[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 )

proof

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;

A3: ex N2 being strict net of L st
( 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