let X, Y be RelStr ; :: thesis: ( not [:X,Y:] is empty implies ( not X is empty & not Y is empty ) )
assume not [:X,Y:] is empty ; :: thesis: ( not X is empty & not Y is empty )
then A1: ex x being object st x in the carrier of [:X,Y:] by XBOOLE_0:def 1;
the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:] by Def2;
hence ( not X is empty & not Y is empty ) by A1, MCART_1:10; :: thesis: verum