theorem :: YELLOW_3:14

for X, Y being RelStr st not [:X,Y:] is empty holds
( not X is empty & not Y is empty )