theorem :: CLASSES4:87

for UN being Universe holds not bool UN in UN by ZFMISC_1:def 1;