let L be non empty RelStr ; :: thesis: lim_inf-Convergence L is (SUBNETS)
let N be net of L; :: according to YELLOW_6:def 24 :: thesis: for b₁ being subnet of N holds
( not b₁ in NetUniv L or for b₂ being Element of the carrier of L holds
( not [N,b₂] in lim_inf-Convergence L or [b₁,b₂] in lim_inf-Convergence L ) )
let M be subnet of N; :: thesis: ( not M in NetUniv L or for b₁ being Element of the carrier of L holds
( not [N,b₁] in lim_inf-Convergence L or [M,b₁] in lim_inf-Convergence L ) )
assume A1: M in NetUniv L ; :: thesis: for b₁ being Element of the carrier of L holds
( not [N,b₁] in lim_inf-Convergence L or [M,b₁] in lim_inf-Convergence L )
let x be Element of L; :: thesis: ( not [N,x] in lim_inf-Convergence L or [M,x] in lim_inf-Convergence L )
assume A2: [N,x] in lim_inf-Convergence L ; :: thesis: [M,x] in lim_inf-Convergence L
lim_inf-Convergence L c= [:(NetUniv L),the carrier of L:] by YELLOW_6:def 21;
then A3: N in NetUniv L by A2, ZFMISC_1:106;
for M1 being subnet of M holds x = lim_inf M1

proof

let M1 be subnet of M; :: thesis: x = lim_inf M1
reconsider M1' = M1 as subnet of N by YELLOW_6:24;
x = lim_inf M1' by A2, A3, Def3;
hence x = lim_inf M1 ; :: thesis: verum

end;

hence [M,x] in lim_inf-Convergence L by A1, Def3; :: thesis: verum