let E be non empty set ; :: thesis: for A being Event of E st A <> {} holds
ex e being Singleton of E st e c= A
let A be Event of E; :: thesis: ( A <> {} implies ex e being Singleton of E st e c= A )
set x = the Element of A;
assume A1: A <> {} ; :: thesis: ex e being Singleton of E st e c= A
then reconsider x = the Element of A as Element of E by TARSKI:def 3;
{x} c= A by A1, ZFMISC_1:31;
hence ex e being Singleton of E st e c= A ; :: thesis: verum