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