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

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