A1: TWOELEMENTSETS {} c= {}

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in TWOELEMENTSETS {} or a in {} )
assume a in TWOELEMENTSETS {} ; :: thesis: a in {}
then consider a1, a2 being set such that
A2: ( a1 in {} & a2 in {} & not a1 = a2 & a = {a1,a2} ) by Th10;
thus a in {} by A2; :: thesis: verum

end;

thus TWOELEMENTSETS {} = {} by A1; :: thesis: verum