let E be set ; :: thesis: for A being Subset of E st A <> {} holds
ex x being Element of E st x in A
let A be Subset of E; :: thesis: ( A <> {} implies ex x being Element of E st x in A )
assume A <> {} ; :: thesis: ex x being Element of E st x in A
then consider x being set such that
A1: x in A by XBOOLE_0:def 1;
x in E by A1, Lm1;
then x is Element of E by Def2;
hence ex x being Element of E st x in A by A1; :: thesis: verum