let S, T be non empty antisymmetric lower-bounded RelStr ; :: thesis: Bottom [:S,T:] = [(Bottom S),(Bottom T)]
A1: ex_sup_of {} ,[:S,T:] by YELLOW_0:42;
A2: {} is_<=_than [(Bottom S),(Bottom T)] by YELLOW_0:6;
for a being Element of [:S,T:] st {} is_<=_than a holds
[(Bottom S),(Bottom T)] <= a

proof

let a be Element of [:S,T:]; :: thesis: ( {} is_<=_than a implies [(Bottom S),(Bottom T)] <= a )
assume {} is_<=_than a ; :: thesis: [(Bottom S),(Bottom T)] <= a
the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2;
then consider s, t being set such that
A3: ( s in the carrier of S & t in the carrier of T & a = [s,t] ) by ZFMISC_1:def 2;
reconsider s = s as Element of S by A3;
reconsider t = t as Element of T by A3;
( Bottom S <= s & Bottom T <= t ) by YELLOW_0:44;
hence [(Bottom S),(Bottom T)] <= a by A3, YELLOW_3:11; :: thesis: verum

end;

hence Bottom [:S,T:] = [(Bottom S),(Bottom T)] by A1, A2, YELLOW_0:def 9; :: thesis: verum