let S, T be non empty antisymmetric upper-bounded RelStr ; :: thesis: Top [:S,T:] = [(Top S),(Top T)]
A1: for a being Element of [:S,T:] st {} is_>=_than a holds
a <= [(Top S),(Top T)]

proof

let a be Element of [:S,T:]; :: thesis: ( {} is_>=_than a implies a <= [(Top S),(Top T)] )
assume {} is_>=_than a ; :: thesis: a <= [(Top S),(Top T)]
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;
( s <= Top S & t <= Top T ) by YELLOW_0:45;
hence a <= [(Top S),(Top T)] by A4, YELLOW_3:11; :: thesis: verum

end;

( ex_inf_of {} ,[:S,T:] & {} is_>=_than [(Top S),(Top T)] ) by YELLOW_0:43;
hence Top [:S,T:] = [(Top S),(Top T)] by A1, YELLOW_0:def 10; :: thesis: verum