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:10;
A1: f is_<=_than {} by YELLOW_0:6;
reconsider f' = f as Function of S,T ;
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 b' = b as Function of S,T by WAYBEL10:10;
reconsider b'' = b', f'' = f as Element of (T |^ the carrier of S) by YELLOW_0:59;
for x being Element of S holds f' . x >= b' . x

proof

let x be Element of S; :: thesis: f' . x >= b' . x
f' . x = (the carrier of S --> (Top T)) . x
.= Top T by FUNCOP_1:13 ;
hence f' . x >= b' . x by YELLOW_0:45; :: thesis: verum

end;

then f' >= b' by YELLOW_2:10;
then f'' >= b'' by WAYBEL10:12;
hence f >= b by YELLOW_0:61; :: thesis: verum

end;

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