theorem Th39: :: MCART_1:51
for X1, X2, X3, X4 being set holds
( ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} ) iff [:X1,X2,X3,X4:] <> {} )