let X, Y be RelStr ; :: thesis: ( not [:X,Y:] is empty implies ( not X is empty & not Y is empty ) )
assume A1: not [:X,Y:] is empty ; :: thesis: ( not X is empty & not Y is empty )
A2: the carrier of [:X,Y:] = [:the carrier of X,the carrier of Y:] by Def2;
not the carrier of [:X,Y:] is empty by A1;
then consider x being set such that
A3: x in the carrier of [:X,Y:] by XBOOLE_0:def 1;
( x `1 in the carrier of X & x `2 in the carrier of Y ) by A2, A3, MCART_1:10;
hence ( not X is empty & not Y is empty ) ; :: thesis: verum