let X, Y, Z be set ; :: thesis: ( Z c= X implies X \/ (Y \ Z) = X \/ Y )
assume A1: Z c= X ; :: thesis: X \/ (Y \ Z) = X \/ Y
A2: X \/ (Y \ Z) c= X \/ Y by XBOOLE_1:9;

now :: thesis: for x being object st x in X \/ Y holds
x in X \/ (Y \ Z)

let x be object ; :: thesis: ( x in X \/ Y implies b₁ in X \/ (Y \ Z) )
assume x in X \/ Y ; :: thesis: b₁ in X \/ (Y \ Z)

per cases then ( x in X or ( x in Y & not x in Z ) or ( x in Y & x in Z ) ) by XBOOLE_0:def 3;

suppose x in X ; :: thesis: b₁ in X \/ (Y \ Z)

hence x in X \/ (Y \ Z) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose ( x in Y & not x in Z ) ; :: thesis: b₁ in X \/ (Y \ Z)

then x in Y \ Z by XBOOLE_0:def 5;
hence x in X \/ (Y \ Z) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose ( x in Y & x in Z ) ; :: thesis: b₁ in X \/ (Y \ Z)

hence x in X \/ (Y \ Z) by A1, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

then X \/ Y c= X \/ (Y \ Z) by TARSKI:def 3;
hence X \/ (Y \ Z) = X \/ Y by A2, XBOOLE_0:def 10; :: thesis: verum