let E be non empty set ; :: thesis: for e being El_ev 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 El_ev 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 ` )
assume A1: e c= A \/ (A ` ) ; :: thesis: ( e c= A or e c= A ` )
ex a being Element of E st
( a in E & e = {a} ) by Th11;
then consider a being Element of E such that
A2: e = {a} ;
a in A \/ (A ` ) by A1, A2, ZFMISC_1:37;
then ( a in A or a in A ` ) by XBOOLE_0:def 3;
hence ( e c= A or e c= A ` ) by A2, ZFMISC_1:37; :: thesis: verum