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 F' = F as Subset of (T |^ the carrier of S) by XBOOLE_1:1;
reconsider sF = sup F' as Function of S,T by Th6;

now

let x, y be Element of S; :: thesis: ( x <= y implies sF . x <= sF . y )
assume A1: x <= y ; :: thesis: sF . x <= sF . y
set G1 = { (f . x) where f is Element of (T |^ the carrier of S) : f in F' } ;
A2: sF . x = "\/" { (f . x) where f is Element of (T |^ the carrier of S) : f in F' } ,T by Th25;
{ (f . x) where f is Element of (T |^ the carrier of S) : f in F' } 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 F' } or a <= sF . y )
assume a in { (f . x) where f is Element of (T |^ the carrier of S) : f in F' } ; :: thesis: a <= sF . y
then consider f' being Element of (T |^ the carrier of S) such that
A3: ( a = f' . x & f' in F' ) ;
reconsider f1 = f' as continuous Function of S,T by A3, Th21;
reconsider f1 = f1 as monotone Function of S,T ;
f' <= sup F' by A3, YELLOW_2:24;
then f1 <= sF by WAYBEL10:12;
then A4: f1 . y <= sF . y by YELLOW_2:10;
f1 . x <= f1 . y by A1, WAYBEL_1:def 2;
hence a <= sF . y by A3, A4, YELLOW_0:def 2; :: thesis: verum

end;

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