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