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