let S, T be non empty RelStr ; ( [: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:]
; YELLOW_0:def 4 ( 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 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 lower-bounded
T is lower-bounded
take
t
; YELLOW_0:def 4 t is_<=_than the carrier of T
thus
t is_<=_than the carrier of T
by A5, A6, YELLOW_3:32; verum