let L be non empty reflexive RelStr ; :: thesis: lim_inf-Convergence L c= Scott-Convergence L
let Ns, xs be object ; :: according to RELAT_1:def 3 :: thesis: ( not [Ns,xs] in lim_inf-Convergence L or [Ns,xs] in Scott-Convergence L )
assume A1: [Ns,xs] in lim_inf-Convergence L ; :: thesis: [Ns,xs] in Scott-Convergence L
A2: lim_inf-Convergence L c= [:(NetUniv L), the carrier of L:] by YELLOW_6:def 18;
then reconsider x = xs as Element of L by A1, ZFMISC_1:87;
Ns in NetUniv L by A2, A1, ZFMISC_1:87;
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 11;
A4: N in NetUniv L by A2, A1, A3, ZFMISC_1:87;
N is subnet of N by YELLOW_6:14;
then x = lim_inf N by A1, A3, A4, Def3;
then x is_S-limit_of N ;
hence [Ns,xs] in Scott-Convergence L by A3, A4, WAYBEL11:def 8; :: thesis: verum