let Z, x1, x2 be set ; :: thesis: ( Z c= {x1,x2} iff ( Z = {} or Z = {x1} or Z = {x2} or Z = {x1,x2} ) )
thus ( not Z c= {x1,x2} or Z = {} or Z = {x1} or Z = {x2} or Z = {x1,x2} ) :: thesis: ( ( Z = {} or Z = {x1} or Z = {x2} or Z = {x1,x2} ) implies Z c= {x1,x2} )

proof

assume that
A1: Z c= {x1,x2} and
A2: Z <> {} and
A3: Z <> {x1} and
A4: Z <> {x2} ; :: thesis: Z = {x1,x2}

now

let z be set ; :: thesis: ( ( z in Z implies z in {x1,x2} ) & ( z in {x1,x2} implies z in Z ) )
thus ( z in Z implies z in {x1,x2} ) by A1, TARSKI:def 3; :: thesis: ( z in {x1,x2} implies z in Z )

A5: now

assume A6: not x1 in Z ; :: thesis: contradiction
consider y being set such that
A7: y in Z and
A8: y <> x2 by A2, A4, Lm13;
y in {x1,x2} by A1, A7, TARSKI:def 3;
hence contradiction by A6, A7, A8, TARSKI:def 2; :: thesis: verum

end;

A9: now

assume A10: not x2 in Z ; :: thesis: contradiction
consider y being set such that
A11: y in Z and
A12: y <> x1 by A2, A3, Lm13;
y in {x1,x2} by A1, A11, TARSKI:def 3;
hence contradiction by A10, A11, A12, TARSKI:def 2; :: thesis: verum

end;

assume z in {x1,x2} ; :: thesis: z in Z
hence z in Z by A5, A9, TARSKI:def 2; :: thesis: verum

end;

hence Z = {x1,x2} by TARSKI:2; :: thesis: verum

end;

thus ( ( Z = {} or Z = {x1} or Z = {x2} or Z = {x1,x2} ) implies Z c= {x1,x2} ) by Th12, XBOOLE_1:2; :: thesis: verum