theorem Th58: :: MCART_1:73

for X1, X2, X3, Y1, Y2, Y3 being set st X1 c= Y1 & X2 c= Y2 & X3 c= Y3 holds
[:X1,X2,X3:] c= [:Y1,Y2,Y3:]