let X, Y, Z be set ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

assume that

A1: X \ Y = X \ Z and

A2: Y c= X and

A3: Z c= X ; :: thesis: 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; :: thesis: verum