let X, Y be set ; :: thesis: (X \/ Y) \ (Y \ X) = X
A3: X \/ (X /\ Y) = X by XBOOLE_1:22;
A4: X \ (Y \ X) = (X \ Y) \/ (X /\ X) by XBOOLE_1:52
.= X by XBOOLE_1:7, XBOOLE_1:8 ;
Y \ (Y \ X) = (Y \ Y) \/ (Y /\ X) by XBOOLE_1:52
.= {} \/ (Y /\ X) by XBOOLE_1:37
.= X /\ Y ;
hence (X \/ Y) \ (Y \ X) = X by XBOOLE_1:42, A3, A4; :: thesis: verum