let X, Y, Z be set ; ( X \ Y = X \ Z & Y c= X & Z c= X implies Y = Z )
assume that
A1:
X \ Y = X \ Z
and
A2:
Y c= X
and
A3:
Z c= X
; Y = Z
A4:
Y \ Z c= X
by A2;
X \ Z misses Y
by A1, XBOOLE_1:106;
then
Y \ Z = {}
by A4, XBOOLE_1:67, XBOOLE_1:81;
then A5:
Y c= Z
by XBOOLE_1:37;
A6:
Z \ Y c= X
by A3;
X \ Y misses Z
by A1, XBOOLE_1:106;
then
Z \ Y = {}
by A6, XBOOLE_1:67, XBOOLE_1:81;
then
Z c= Y
by XBOOLE_1:37;
hence
Y = Z
by A5, XBOOLE_0:def 10; verum