let S, T be non empty complete Scott TopLattice; :: thesis: Bottom (ContMaps (S,T)) = S --> (Bottom T)
set L = ContMaps (S,T);
reconsider f = S --> (Bottom 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 [(f . i),(b . i)] in the InternalRel of T

proof

let i be Element of S; :: thesis: [(f . i),(b . i)] in the InternalRel of T
f . i = ( the carrier of S --> (Bottom T)) . i
.= Bottom T by FUNCOP_1:7 ;
then f9 . i <= b9 . i by YELLOW_0:44;
hence [(f . i),(b . 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:30;
hence Bottom (ContMaps (S,T)) = S --> (Bottom T) by YELLOW_0:def 11; :: thesis: verum