let X, Y, Z be set ; :: thesis: ( X \ Y = X \ Z & Y c= X & Z c= X implies Y = Z )
assume A1: ( X \ Y = X \ Z & Y c= X & Z c= X ) ; :: thesis: Y = Z
then A2: ( X \ Y misses Z & Y \/ X = X & X \ Z misses Y & Z \/ X = X ) by XBOOLE_1:12, XBOOLE_1:106;
then ( Z \ Y c= X & Y \ Z c= X ) by A1, XBOOLE_1:43;
then ( Z \ Y = {} & Y \ Z = {} ) by A2, XBOOLE_1:67, XBOOLE_1:81;
then ( Z c= Y & Y c= Z ) by XBOOLE_1:37;
hence Y = Z by XBOOLE_0:def 10; :: thesis: verum