let X, Y, Z be set ; :: thesis: ( Y misses Z implies (X \ Y) \/ Z = (X \/ Z) \ Y )
assume A1: Y misses Z ; :: thesis: (X \ Y) \/ Z = (X \/ Z) \ Y
thus (X \/ Z) \ Y = (X \ Y) \/ (Z \ Y) by Th42
.= (X \ Y) \/ Z by A1, Th83 ; :: thesis: verum