let N be constant net of R; :: according to YELLOW_6:def 20 :: thesis: ( not N in NetUniv R or [N,(the_value_of N)] in Scott-Convergence R )
assume A1: N in NetUniv R ; :: thesis: [N,(the_value_of N)] in Scott-Convergence R
then consider M being strict net of R such that
A2: M = N and
the carrier of M in the_universe_of the carrier of R by YELLOW_6:def 11;
the_value_of M is_S-limit_of M by A2, Th24;
hence [N,(the_value_of N)] in Scott-Convergence R by A1, A2, Def8; :: thesis: verum