let S be non empty RelStr ; :: thesis: for T being non empty antisymmetric lower-bounded RelStr holds Bottom (T |^ the carrier of S) = S --> (Bottom T)
let T be non empty antisymmetric lower-bounded RelStr ; :: thesis: Bottom (T |^ the carrier of S) = S --> (Bottom T)
set L = T |^ the carrier of S;
reconsider f = S --> (Bottom T) as Element of (T |^ the carrier of S) by Th19;
A1: f is_>=_than {} by YELLOW_0:6;
reconsider f' = f as Function of S,T ;
for b being Element of (T |^ the carrier of S) st b is_>=_than {} holds
f <= b

proof

let b be Element of (T |^ the carrier of S); :: thesis: ( b is_>=_than {} implies f <= b )
assume b is_>=_than {} ; :: thesis: f <= b
reconsider b' = b as Function of S,T by Th19;
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 --> (Bottom T)) . x by BORSUK_1:def 2
.= Bottom T by FUNCOP_1:13 ;
hence f' . x <= b' . x by YELLOW_0:44; :: thesis: verum

end;

then f' <= b' by YELLOW_2:10;
hence f <= b by WAYBEL10:12; :: thesis: verum

end;

then f = "\/" {} ,(T |^ the carrier of S) by A1, YELLOW_0:30;
hence Bottom (T |^ the carrier of S) = S --> (Bottom T) by YELLOW_0:def 11; :: thesis: verum