theorem :: YELLOW10:1

for S, T being non empty RelStr st [:S,T:] is upper-bounded holds
( S is upper-bounded & T is upper-bounded )