let E be non empty set ; :: thesis: for e being Singleton of E
for A being Event of E holds
( not e c= A \/ (A `) or e c= A or e c= A ` )
let e be Singleton of E; :: thesis: for A being Event of E holds
( not e c= A \/ (A `) or e c= A or e c= A ` )
let A be Event of E; :: thesis: ( not e c= A \/ (A `) or e c= A or e c= A ` )
ex a being Element of E st
( a in E & e = {a} ) by Th6;
then consider a being Element of E such that
A1: e = {a} ;
assume e c= A \/ (A `) ; :: thesis: ( e c= A or e c= A ` )
then a in A \/ (A `) by A1, ZFMISC_1:31;
then ( a in A or a in A ` ) by XBOOLE_0:def 3;
hence ( e c= A or e c= A ` ) by A1, ZFMISC_1:31; :: thesis: verum