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 b_{1} being subnet of N holds

( not b_{1} in NetUniv L or for b_{2} being Element of the carrier of L holds

( not [N,b_{2}] in lim_inf-Convergence L or [b_{1},b_{2}] in lim_inf-Convergence L ) )

let M be subnet of N; :: thesis: ( not M in NetUniv L or for b_{1} being Element of the carrier of L holds

( not [N,b_{1}] in lim_inf-Convergence L or [M,b_{1}] in lim_inf-Convergence L ) )

assume A1: M in NetUniv L ; :: thesis: for b_{1} being Element of the carrier of L holds

( not [N,b_{1}] in lim_inf-Convergence L or [M,b_{1}] 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

let N be net of L; :: according to YELLOW_6:def 21 :: thesis: for b

( not b

( not [N,b

let M be subnet of N; :: thesis: ( not M in NetUniv L or for b

( not [N,b

assume A1: M in NetUniv L ; :: thesis: for b

( not [N,b

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

hence
[M,x] in lim_inf-Convergence L
by A1, Def3; :: thesis: verum
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;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