let T be complete continuous Scott TopLattice; :: thesis: for x being Element of T
for N being net of T st N in NetUniv T holds
( x is_S-limit_of N iff x in Lim N )
let x be Element of T; :: thesis: for N being net of T st N in NetUniv T holds
( x is_S-limit_of N iff x in Lim N )
let N be net of T; :: thesis: ( N in NetUniv T implies ( x is_S-limit_of N iff x in Lim N ) )
assume A1: N in NetUniv T ; :: thesis: ( x is_S-limit_of N iff x in Lim N )
A2: Convergence (ConvergenceSpace (Scott-Convergence T)) = Scott-Convergence T by YELLOW_6:44;
consider M being strict net of T such that
A3: M = N and
the carrier of M in the_universe_of the carrier of T by A1, YELLOW_6:def 11;
TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) by Th32;
then A4: Convergence T = Convergence (ConvergenceSpace (Scott-Convergence T)) by Lm8;
thus ( x is_S-limit_of N implies x in Lim N ) :: thesis: ( x in Lim N implies x is_S-limit_of N )
proof
assume x is_S-limit_of N ; :: thesis: x in Lim N
then [N,x] in Convergence T by A1, A2, A3, A4, Def8;
hence x in Lim N by YELLOW_6:def 19; :: thesis: verum
end;
assume x in Lim N ; :: thesis: x is_S-limit_of N
then [M,x] in Scott-Convergence T by A1, A2, A3, A4, YELLOW_6:def 19;
hence x is_S-limit_of N by A1, A3, Def8; :: thesis: verum