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