let X, Y be set ; :: thesis: X \/ Y = X \+\ (Y \ X)
A1: (Y \ X) \ X = Y \ (X \/ X) by Th41
.= Y \ X ;
X \ (Y \ X) = (X \ Y) \/ (X /\ X) by Th52
.= X by Th12, Th36 ;
hence X \/ Y = X \+\ (Y \ X) by A1, Th39; :: thesis: verum