theorem Th95: :: ZFMISC_1:96

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