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 :: thesis: for x, y being Element of S st x <= y holds
sF . x <= sF . y

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:22;
then f1 <= sF by WAYBEL10:11;
then A5: f1 . y <= sF . y by YELLOW_2:9;
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