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;
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 [(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:13 ;
then f' . i <= b' . i by YELLOW_0:44;
hence [(f . i),(b . 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:30;
hence Bottom (ContMaps S,T) = S --> (Bottom T) by YELLOW_0:def 11; :: thesis: verum