let L be non empty reflexive RelStr ; :: thesis: lim_inf-Convergence L c= Scott-Convergence L
let Ns, xs be set ; :: according to RELAT_1:def 3 :: thesis: ( not [Ns,xs] in lim_inf-Convergence L or [Ns,xs] in Scott-Convergence L )
A1: lim_inf-Convergence L c= [:(NetUniv L),the carrier of L:] by YELLOW_6:def 21;
assume A2: [Ns,xs] in lim_inf-Convergence L ; :: thesis: [Ns,xs] in Scott-Convergence L
then Ns in NetUniv L by A1, ZFMISC_1:106;
then consider N being strict net of L such that
A3: N = Ns and
the carrier of N in the_universe_of the carrier of L by YELLOW_6:def 14;
A4: N in NetUniv L by A1, A2, A3, ZFMISC_1:106;
reconsider x = xs as Element of L by A1, A2, ZFMISC_1:106;
N is subnet of N by YELLOW_6:23;
then x = lim_inf N by A2, A3, A4, Def3;
then x is_S-limit_of N by WAYBEL11:def 7;
hence [Ns,xs] in Scott-Convergence L by A3, A4, WAYBEL11:def 8; :: thesis: verum