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;
reconsider f9 = f as Function of S,T ;
A1: 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 )
reconsider b9 = b as Function of S,T by Th21;
assume b is_<=_than {} ; :: thesis: f >= b
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:7 ;
then f9 . i >= b9 . i by YELLOW_0:45;
hence [(b . i),(f . i)] in the InternalRel of T ; :: thesis: verum

end;

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

end;

f is_<=_than {} ;
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