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

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