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

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