let a be non empty set ; :: thesis: ( a <> {{} } & {} in a implies ex b being set st
( b in a & b <> {} ) )
assume that
A1: a <> {{} } and
A2: {} in a ; :: thesis: ex b being set st
( b in a & b <> {} )
assume A3: for b being set st b in a holds
b = {} ; :: thesis: contradiction
a = {{} }

proof

thus a c= {{} } :: according to XBOOLE_0:def 10 :: thesis: {{} } c= a

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in a or x in {{} } )
assume x in a ; :: thesis: x in {{} }
then x = {} by A3;
hence x in {{} } by TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {{} } or x in a )
assume x in {{} } ; :: thesis: x in a
hence x in a by A2, TARSKI:def 1; :: thesis: verum

end;

hence contradiction by A1; :: thesis: verum