let E be non empty set ; :: thesis: for e being El_ev of E
for A being Event of E holds
( e misses A or e /\ A = e )
let e be El_ev of E; :: thesis: for A being Event of E holds
( e misses A or e /\ A = e )
let A be Event of E; :: thesis: ( e misses A or e /\ A = e )
A1: e /\ E = e by XBOOLE_1:28;
A \/ (A ` ) = [#] E by SUBSET_1:25;
then e = (e /\ A) \/ (e /\ (A ` )) by A1, XBOOLE_1:23;
then e /\ A c= e by XBOOLE_1:7;
then ( e /\ A = {} or e /\ A = e ) by Th1;
hence ( e misses A or e /\ A = e ) by XBOOLE_0:def 7; :: thesis: verum