let a be object ; :: thesis: for A, B being set st A c= B & B c= A \/ {a} & not A \/ {a} = B holds
A = B
let A, B 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
not a in B
proof
assume a in B ; :: thesis: contradiction
then {a} c= B by Lm1;
hence contradiction by A1, A2, A3, XBOOLE_1:8; :: thesis: verum
end;
hence contradiction by A2, Th134, A1, A4; :: thesis: verum