let X, Y be set ; :: thesis: X \/ Y = (X \+\ Y) \/ (X /\ Y)
thus X \/ Y = ((X \ Y) \/ (X /\ Y)) \/ Y by Th51
.= (X \ Y) \/ ((X /\ Y) \/ Y) by Th4
.= (X \ Y) \/ Y by Th22
.= (X \ Y) \/ ((Y \ X) \/ (Y /\ X)) by Th51
.= (X \+\ Y) \/ (X /\ Y) by Th4 ; :: thesis: verum