let X, Y be set ; :: thesis: X \/ (Y \ X) = X \/ Y

thus X \/ (Y \ X) c= X \/ Y :: according to XBOOLE_0:def 10 :: thesis: X \/ Y c= X \/ (Y \ X)

assume x in X \/ Y ; :: thesis: x in X \/ (Y \ X)

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

then ( x in X or x in Y \ X ) by XBOOLE_0:def 5;

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

thus X \/ (Y \ X) c= X \/ Y :: according to XBOOLE_0:def 10 :: thesis: X \/ Y c= X \/ (Y \ X)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X \/ Y or x in X \/ (Y \ X) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X \/ (Y \ X) or x in X \/ Y )

assume x in X \/ (Y \ X) ; :: thesis: x in X \/ Y

then ( x in X or x in Y \ X ) by XBOOLE_0:def 3;

then ( x in X or x in Y ) by XBOOLE_0:def 5;

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

end;assume x in X \/ (Y \ X) ; :: thesis: x in X \/ Y

then ( x in X or x in Y \ X ) by XBOOLE_0:def 3;

then ( x in X or x in Y ) by XBOOLE_0:def 5;

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

assume x in X \/ Y ; :: thesis: x in X \/ (Y \ X)

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

then ( x in X or x in Y \ X ) by XBOOLE_0:def 5;

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