let A, B, a be set ; :: thesis: ( A c= B & B c= A \/ {a} & not A \/ {a} = B implies A = B )
assume that
A1: A c= B and
A2: B c= A \/ {a} ; :: thesis: ( A \/ {a} = B or A = B )
assume that
A3: A \/ {a} <> B and
A4: A <> B ; :: thesis: contradiction
A5: not A \/ {a} c= B by A2, A3, XBOOLE_0:def 10;
A6: not a in B

proof

assume a in B ; :: thesis: contradiction
then {a} c= B by ZFMISC_1:31;
hence contradiction by A1, A5, XBOOLE_1:8; :: thesis: verum

end;

not B c= A by A1, A4, XBOOLE_0:def 10;
hence contradiction by A2, A6, SETWISEO:3; :: thesis: verum