let S, T be non empty complete Scott TopLattice; 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
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; verum