theorem Th94: :: ZFMISC_1:95

for X, Y, Z being set st X c= Y holds
( [:X,Z:] c= [:Y,Z:] & [:Z,X:] c= [:Z,Y:] )