TWOELEMENTSETS {} c= {}

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in TWOELEMENTSETS {} or a in {} )
assume a in TWOELEMENTSETS {} ; :: thesis: a in {}
then ex a1, a2 being object st
( a1 in {} & a2 in {} & not a1 = a2 & a = {a1,a2} ) by Th8;
hence a in {} ; :: thesis: verum

end;

hence TWOELEMENTSETS {} = {} ; :: thesis: verum