let S be non empty RelStr ; :: thesis: for T being non empty reflexive antisymmetric upper-bounded RelStr holds Top (MonMaps (S,T)) = S --> (Top T)
let T be non empty reflexive antisymmetric upper-bounded RelStr ; :: thesis: Top (MonMaps (S,T)) = S --> (Top T)
set L = MonMaps (S,T);
reconsider f = S --> (Top T) as Element of (MonMaps (S,T)) by WAYBEL10:9;
reconsider f9 = f as Function of S,T ;
A1: for b being Element of (MonMaps (S,T)) st b is_<=_than {} holds
f >= b

proof

let b be Element of (MonMaps (S,T)); :: thesis: ( b is_<=_than {} implies f >= b )
assume b is_<=_than {} ; :: thesis: f >= b
reconsider b9 = b as Function of S,T by WAYBEL10:9;
reconsider b99 = b9, f99 = f as Element of (T |^ the carrier of S) by YELLOW_0:58;
for x being Element of S holds f9 . x >= b9 . x

proof

let x be Element of S; :: thesis: f9 . x >= b9 . x
f9 . x = ( the carrier of S --> (Top T)) . x
.= Top T by FUNCOP_1:7 ;
hence f9 . x >= b9 . x by YELLOW_0:45; :: thesis: verum

end;

then f9 >= b9 by YELLOW_2:9;
then f99 >= b99 by WAYBEL10:11;
hence f >= b by YELLOW_0:60; :: thesis: verum

end;

f is_<=_than {} ;
then f = "/\" ({},(MonMaps (S,T))) by A1, YELLOW_0:31;
hence Top (MonMaps (S,T)) = S --> (Top T) by YELLOW_0:def 12; :: thesis: verum