let X, X9, Y, Y9 be set ; :: thesis: ( X9 \/ Y9 = X \/ Y & X misses X9 & Y misses Y9 implies X = Y9 )
assume A1: X9 \/ Y9 = X \/ Y ; :: thesis: ( not X misses X9 or not Y misses Y9 or X = Y9 )
assume ( X misses X9 & Y misses Y9 ) ; :: thesis: X = Y9
then A2: ( X /\ X9 = {} & Y /\ Y9 = {} ) ;
thus X = X /\ (X9 \/ Y9) by A1, Th7, Th28
.= (X /\ X9) \/ (X /\ Y9) by Th23
.= (X \/ Y) /\ Y9 by A2, Th23
.= Y9 by A1, Th7, Th28 ; :: thesis: verum