let X, Y be set ; :: thesis: (X \/ Y) \ (X /\ Y) = (X \ Y) \/ (Y \ X)
for x being object holds
( x in (X \/ Y) \ (X /\ Y) iff x in (X \ Y) \/ (Y \ X) )

proof

let x be object ; :: thesis: ( x in (X \/ Y) \ (X /\ Y) iff x in (X \ Y) \/ (Y \ X) )
thus ( x in (X \/ Y) \ (X /\ Y) implies x in (X \ Y) \/ (Y \ X) ) :: thesis: ( x in (X \ Y) \/ (Y \ X) implies x in (X \/ Y) \ (X /\ Y) )

proof

assume A1: x in (X \/ Y) \ (X /\ Y) ; :: thesis: x in (X \ Y) \/ (Y \ X)
then not x in X /\ Y by XBOOLE_0:def 5;
then A2: ( not x in X or not x in Y ) by XBOOLE_0:def 4;
x in X \/ Y by A1, XBOOLE_0:def 5;
then ( x in X or x in Y ) by XBOOLE_0:def 3;
then ( x in X \ Y or x in Y \ X ) by A2, XBOOLE_0:def 5;
hence x in (X \ Y) \/ (Y \ X) by XBOOLE_0:def 3; :: thesis: verum

end;

assume x in (X \ Y) \/ (Y \ X) ; :: thesis: x in (X \/ Y) \ (X /\ Y)
then ( x in X \ Y or x in Y \ X ) by XBOOLE_0:def 3;
then ( ( x in X & not x in Y ) or ( x in Y & not x in X ) ) by XBOOLE_0:def 5;
then ( not x in X /\ Y & x in X \/ Y ) by XBOOLE_0:def 3, XBOOLE_0:def 4;
hence x in (X \/ Y) \ (X /\ Y) by XBOOLE_0:def 5; :: thesis: verum

end;

hence (X \/ Y) \ (X /\ Y) = (X \ Y) \/ (Y \ X) by TARSKI:2; :: thesis: verum