let o be object ; :: thesis: for S being set holds
( not S c= {o} or S = {} or S = {o} )
let S be set ; :: thesis: ( not S c= {o} or S = {} or S = {o} )
assume AS1: S c= {o} ; :: thesis: ( S = {} or S = {o} )
assume AS2: S <> {} ; :: thesis: S = {o}
set u = the Element of S;
A: the Element of S in S by AS2;

now :: thesis: for x being object st x in {o} holds
x in S

let x be object ; :: thesis: ( x in {o} implies x in S )
assume x in {o} ; :: thesis: x in S
then x = o by TARSKI:def 1;
hence x in S by A, AS1, TARSKI:def 1; :: thesis: verum

end;

hence S = {o} by AS1, TARSKI:2; :: thesis: verum