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) )

for x being object holds

( x in (X \/ Y) \ (X /\ Y) iff x in (X \ Y) \/ (Y \ X) )

proof

hence
(X \/ Y) \ (X /\ Y) = (X \ Y) \/ (Y \ X)
by TARSKI:2; :: thesis: verum
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) )

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;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
x in (X \ Y) \/ (Y \ X)
; :: thesis: x in (X \/ Y) \ (X /\ Y)
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;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

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