let S, T be non empty antisymmetric lower-bounded RelStr ; :: thesis: Bottom [:S,T:] = [(Bottom S),(Bottom T)]
A1: 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 object such that
A2: s in the carrier of S and
A3: t in the carrier of T and
A4: a = [s,t] by ZFMISC_1:def 2;
reconsider t = t as Element of T by A3;
reconsider s = s as Element of S by A2;
( Bottom S <= s & Bottom T <= t ) by YELLOW_0:44;
hence [(Bottom S),(Bottom T)] <= a by A4, YELLOW_3:11; :: thesis: verum
end;
( ex_sup_of {} ,[:S,T:] & {} is_<=_than [(Bottom S),(Bottom T)] ) by YELLOW_0:42;
hence Bottom [:S,T:] = [(Bottom S),(Bottom T)] by A1, YELLOW_0:def 9; :: thesis: verum