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 )
assume A1: A <> {} ; :: thesis: ex e being El_ev of E st e c= A
consider x being Element of A;
reconsider x = x as Element of E by A1, TARSKI:def 3;
A2: {x} is El_ev of E by Th7;
{x} c= A by A1, ZFMISC_1:37;
hence ex e being El_ev of E st e c= A by A2; :: thesis: verum