let E be non empty set ; :: thesis: for e being Singleton of E
for A being Event of E holds
( e misses A or e /\ A = e )
let e be Singleton 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 )
( e /\ E = e & A \/ (A `) = [#] E ) by SUBSET_1:10, XBOOLE_1:28;
then e = (e /\ A) \/ (e /\ (A `)) by 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 ) ; :: thesis: verum