theorem :: ZFMISC_1:93

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