let X, Y be set ; :: thesis: X \+\ Y = (X \/ Y) \ (X /\ Y)
thus X \+\ Y = (X \ (X /\ Y)) \/ (Y \ X) by Th47
.= (X \ (X /\ Y)) \/ (Y \ (X /\ Y)) by Th47
.= (X \/ Y) \ (X /\ Y) by Th42 ; :: thesis: verum