let X, Y, Z be set ; :: thesis: (X \/ Y) \/ Z = (X \/ Z) \/ (Y \/ Z)
(X \/ Y) \/ Z = X \/ ((Z \/ Z) \/ Y) by Th4
.= X \/ (Z \/ (Z \/ Y)) by Th4
.= (X \/ Z) \/ (Y \/ Z) by Th4 ;
hence (X \/ Y) \/ Z = (X \/ Z) \/ (Y \/ Z) ; :: thesis: verum