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