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