let X, Y be set ; :: thesis: X \/ Y = (X \+\ Y) \+\ (X /\ Y)
X /\ Y misses X \+\ Y by Lm4;
then ( (X \+\ Y) \ (X /\ Y) = X \+\ Y & (X /\ Y) \ (X \+\ Y) = X /\ Y ) by Th83;
hence X \/ Y = (X \+\ Y) \+\ (X /\ Y) by Th93; :: thesis: verum