let a, A be set ; :: thesis: ( A /\ {a} <> {} implies a in A )
assume A /\ {a} <> {} ; :: thesis: a in A
then A meets {a} by XBOOLE_0:def 7;
hence a in A by ZFMISC_1:56; :: thesis: verum