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 object ; :: 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 object ; :: 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