theorem :: ZFMISC_1:93

for X, Y being set st X c= [:X,Y:] holds
X = {}