let I be set ; :: thesis: for Z, V, X, Y being ManySortedSet of I st Z \/ V = X \/ Y & X misses Z & Y misses V holds
( X = V & Y = Z )
let Z, V, X, Y be ManySortedSet of I; :: thesis: ( Z \/ V = X \/ Y & X misses Z & Y misses V implies ( X = V & Y = Z ) )
assume A1: Z \/ V = X \/ Y ; :: thesis: ( not X misses Z or not Y misses V or ( X = V & Y = Z ) )
then A2: V c= X \/ Y by Th16;
A3: Z c= X \/ Y by A1, Th16;
assume ( X misses Z & Y misses V ) ; :: thesis: ( X = V & Y = Z )
then A4: ( X /\ Z = [[0]] I & Y /\ V = [[0]] I ) by Th121;
X c= Z \/ V by A1, Th16;
hence X = X /\ (Z \/ V) by Th25
.= (X /\ Z) \/ (X /\ V) by Th38
.= (X \/ Y) /\ V by A4, Th38
.= V by A2, Th25 ;
:: thesis: Y = Z
Y c= Z \/ V by A1, Th16;
hence Y = Y /\ (Z \/ V) by Th25
.= (Y /\ Z) \/ (Y /\ V) by Th38
.= (X \/ Y) /\ Z by A4, Th38
.= Z by A3, Th25 ;
:: thesis: verum