theorem :: YELLOW10:2
for S, T being non empty RelStr st [:S,T:] is lower-bounded holds
( S is lower-bounded & T is lower-bounded )