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 )
A1: lim_inf-Convergence L c= [:(NetUniv L), the carrier of L:] by YELLOW_6:def 18;
assume [N,x] in lim_inf-Convergence L ; :: thesis: N in NetUniv L
hence N in NetUniv L by A1, ZFMISC_1:87; :: thesis: verum