let X, Y, Z be set ; :: thesis: ( X \/ Y = Z \/ Y & X misses Y & Z misses Y implies X = Z )
assume that
A1: X \/ Y = Z \/ Y and
A2: X /\ Y = {} and
A3: Z /\ Y = {} ; :: according to XBOOLE_0:def 7 :: thesis: X = Z
thus X c= Z :: according to XBOOLE_0:def 10 :: thesis: Z c= X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Z )
assume A4: x in X ; :: thesis: x in Z
X c= Z \/ Y by A1, Th7;
then A5: x in Z \/ Y by A4;
not x in Y by A2, A4, XBOOLE_0:def 4;
hence x in Z by A5, XBOOLE_0:def 3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Z or x in X )
assume A6: x in Z ; :: thesis: x in X
Z c= X \/ Y by A1, Th7;
then A7: x in X \/ Y by A6;
not x in Y by A3, A6, XBOOLE_0:def 4;
hence x in X by A7, XBOOLE_0:def 3; :: thesis: verum