theorem :: EUCLID_9:7

for B being Subset of (Euclid 0) holds
( B = {} or B = {{}} ) by EUCLID:77, ZFMISC_1:33;