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

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

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

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

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

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

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

proof

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

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

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

hence x in X by XBOOLE_0:def 4, XBOOLE_0:def 5; :: thesis: verum

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

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

hence x in X by XBOOLE_0:def 4, XBOOLE_0:def 5; :: thesis: verum

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

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

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

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