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