theorem :: ZFMISC_1:94

for X, Y, Z being set st Z <> {} & ( [:X,Z:] c= [:Y,Z:] or [:Z,X:] c= [:Z,Y:] ) holds
X c= Y