let L be non empty RelStr ; :: thesis: for N, x being set st [N,x] in lim_inf-Convergence L holds
N in NetUniv L
let N, x be set ; :: thesis: ( [N,x] in lim_inf-Convergence L implies N in NetUniv L )
assume A1: [N,x] in lim_inf-Convergence L ; :: thesis: N in NetUniv L
lim_inf-Convergence L c= [:(NetUniv L),the carrier of L:] by YELLOW_6:def 21;
hence N in NetUniv L by A1, ZFMISC_1:106; :: thesis: verum