let S be non empty RelStr ; :: thesis:
let T be non empty reflexive antisymmetric lower-bounded RelStr ; :: thesis:
set L = MonMaps (S,T);
reconsider f = S --> (Bottom 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

let b be Element of (MonMaps (S,T)); :: thesis:
assume b is_>=_than {} ; :: thesis:
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

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

end;

end;