let X, Y be set ; :: thesis: X = (X \ Y) \/ (X /\ Y)
reconsider x = X \ Y as Subset of X ;
X = x \/ (X \ x) by XBOOLE_1:45
.= x \/ (X /\ Y) by XBOOLE_1:48 ;
hence X = (X \ Y) \/ (X /\ Y) ; :: thesis: verum