let S, T be non empty antisymmetric upper-bounded RelStr ; :: thesis: Top [:S,T:] = [(Top S),(Top T)]
A1: ex_inf_of {} ,[:S,T:] by YELLOW_0:43;
A2: {} is_>=_than [(Top S),(Top T)] by YELLOW_0:6;
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 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;
( s <= Top S & t <= Top T ) by YELLOW_0:45;
hence a <= [(Top S),(Top T)] by A3, YELLOW_3:11; :: thesis: verum

end;

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