let S, T be non empty RelStr ; :: thesis: ( [:S,T:] is upper-bounded implies ( S is upper-bounded & T is upper-bounded ) )
given x being Element of [:S,T:] such that A1: x is_>=_than the carrier of [:S,T:] ; :: according to YELLOW_0:def 5 :: thesis: ( S is upper-bounded & T is upper-bounded )
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: x = [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;
A5: ( the carrier of S c= the carrier of S & the carrier of T c= the carrier of T ) ;
A6: [s,t] is_>=_than [: the carrier of S, the carrier of T:] by A1, A4;
thus S is upper-bounded :: thesis: T is upper-bounded

proof

take s ; :: according to YELLOW_0:def 5 :: thesis: the carrier of S is_<=_than s
thus the carrier of S is_<=_than s by A5, A6, YELLOW_3:29; :: thesis: verum

end;

take t ; :: according to YELLOW_0:def 5 :: thesis: the carrier of T is_<=_than t
thus the carrier of T is_<=_than t by A5, A6, YELLOW_3:29; :: thesis: verum