let S, T be non empty complete Scott TopLattice; :: thesis: Top (ContMaps S,T) = S --> (Top T)
set L = ContMaps S,T;
reconsider f = S --> (Top T) as Element of (ContMaps S,T) by Th21;
A1: f is_<=_than {} by YELLOW_0:6;
reconsider f' = f as Function of S,T ;
for b being Element of (ContMaps S,T) st b is_<=_than {} holds
f >= b

proof

let b be Element of (ContMaps S,T); :: thesis: ( b is_<=_than {} implies f >= b )
assume b is_<=_than {} ; :: thesis: f >= b
reconsider b' = b as Function of S,T by Th21;
for i being Element of S holds [(b . i),(f . i)] in the InternalRel of T

proof

let i be Element of S; :: thesis: [(b . i),(f . i)] in the InternalRel of T
f . i = (the carrier of S --> (Top T)) . i
.= Top T by FUNCOP_1:13 ;
then f' . i >= b' . i by YELLOW_0:45;
hence [(b . i),(f . i)] in the InternalRel of T by ORDERS_2:def 9; :: thesis: verum

end;

hence f >= b by Th20; :: thesis: verum

end;

then f = "/\" {} ,(ContMaps S,T) by A1, YELLOW_0:31;
hence Top (ContMaps S,T) = S --> (Top T) by YELLOW_0:def 12; :: thesis: verum