union ('not' {{}}) = union {{}} by Th66
.= {} by ZFMISC_1:25 ;
hence 'not' {{}} c= {{}} by ZFMISC_1:1, ZFMISC_1:82; :: according to XBOOLE_0:def 10 :: thesis: {{}} c= 'not' {{}}
{} in 'not' {{}} by COH_SP:1;
hence {{}} c= 'not' {{}} by ZFMISC_1:31; :: thesis: verum