let L be non empty RelStr ; :: thesis: lim_inf-Convergence L is (SUBNETS)
let N be net of L; :: according to YELLOW_6:def 21 :: thesis: for b1 being subnet of N holds
( not b1 in NetUniv L or for b2 being Element of the carrier of L holds
( not [N,b2] in lim_inf-Convergence L or [b1,b2] in lim_inf-Convergence L ) )
let M be subnet of N; :: thesis: ( not M in NetUniv L or for b1 being Element of the carrier of L holds
( not [N,b1] in lim_inf-Convergence L or [M,b1] in lim_inf-Convergence L ) )
assume A1: M in NetUniv L ; :: thesis: for b1 being Element of the carrier of L holds
( not [N,b1] in lim_inf-Convergence L or [M,b1] 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 18;
then A3: N in NetUniv L by A2, ZFMISC_1:87;
for M1 being subnet of M holds x = lim_inf M1
proof
let M1 be subnet of M; :: thesis: x = lim_inf M1
reconsider M19 = M1 as subnet of N by YELLOW_6:15;
x = lim_inf M19 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