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