let S, T be complete Scott TopLattice; :: thesis: for F being non empty Subset of (ContMaps S,T) holds "\/" F,(T |^ the carrier of S) is monotone Function of S,T
let F be non empty Subset of (ContMaps S,T); :: thesis: "\/" F,(T |^ the carrier of S) is monotone Function of S,T
ContMaps S,T is full SubRelStr of T |^ the carrier of S by Def3;
then the carrier of (ContMaps S,T) c= the carrier of (T |^ the carrier of S) by YELLOW_0:def 13;
then reconsider F9 = F as Subset of (T |^ the carrier of S) by XBOOLE_1:1;
reconsider sF = sup F9 as Function of S,T by Th6;

now

let x, y be Element of S; :: thesis: ( x <= y implies sF . x <= sF . y )
set G1 = { (f . x) where f is Element of (T |^ the carrier of S) : f in F9 } ;
assume A1: x <= y ; :: thesis: sF . x <= sF . y
A2: { (f . x) where f is Element of (T |^ the carrier of S) : f in F9 } is_<=_than sF . y

proof

let a be Element of T; :: according to LATTICE3:def 9 :: thesis: ( not a in { (f . x) where f is Element of (T |^ the carrier of S) : f in F9 } or a <= sF . y )
assume a in { (f . x) where f is Element of (T |^ the carrier of S) : f in F9 } ; :: thesis: a <= sF . y
then consider f9 being Element of (T |^ the carrier of S) such that
A3: a = f9 . x and
A4: f9 in F9 ;
reconsider f1 = f9 as continuous Function of S,T by A4, Th21;
reconsider f1 = f1 as monotone Function of S,T ;
f9 <= sup F9 by A4, YELLOW_2:24;
then f1 <= sF by WAYBEL10:12;
then A5: f1 . y <= sF . y by YELLOW_2:10;
f1 . x <= f1 . y by A1, WAYBEL_1:def 2;
hence a <= sF . y by A3, A5, YELLOW_0:def 2; :: thesis: verum

end;

sF . x = "\/" { (f . x) where f is Element of (T |^ the carrier of S) : f in F9 } ,T by Th25;
hence sF . x <= sF . y by A2, YELLOW_0:32; :: thesis: verum

end;

hence "\/" F,(T |^ the carrier of S) is monotone Function of S,T by WAYBEL_1:def 2; :: thesis: verum