let S, T be complete continuous Scott TopLattice; :: thesis: for f being Function of S,T st ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) holds
f is directed-sups-preserving
let f be Function of S,T; :: thesis: ( ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) implies f is directed-sups-preserving )
assume for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ; :: thesis: f is directed-sups-preserving
then for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) ) by Th14;
then f is continuous by Lm15;
hence f is directed-sups-preserving ; :: thesis: verum