let S, T be non empty RelStr ; :: thesis: ( [:S,T:] is lower-bounded implies ( S is lower-bounded & T is lower-bounded ) )
given x being Element of [:S,T:] such that A1: x is_<=_than the carrier of [:S,T:] ; :: according to YELLOW_0:def 4 :: thesis: ( S is lower-bounded & T is lower-bounded )
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
A2: ( s in the carrier of S & t in the carrier of T & x = [s,t] ) by ZFMISC_1:def 2;
reconsider s = s as Element of S by A2;
reconsider t = t as Element of T by A2;
A3: ( the carrier of S c= the carrier of S & the carrier of T c= the carrier of T ) ;
A4: [s,t] is_<=_than [:the carrier of S,the carrier of T:] by A1, A2, YELLOW_3:def 2;
thus S is lower-bounded :: thesis: T is lower-bounded

proof

take s ; :: according to YELLOW_0:def 4 :: thesis: s is_<=_than the carrier of S
thus s is_<=_than the carrier of S by A3, A4, YELLOW_3:32; :: thesis: verum

end;

take t ; :: according to YELLOW_0:def 4 :: thesis: t is_<=_than the carrier of T
thus t is_<=_than the carrier of T by A3, A4, YELLOW_3:32; :: thesis: verum