theorem :: MCART_1:33

for X1, X2, X3, Y1, Y2, Y3 being set st [:X1,X2,X3:] <> {} & [:X1,X2,X3:] = [:Y1,Y2,Y3:] holds
( X1 = Y1 & X2 = Y2 & X3 = Y3 )