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 ) )
assume ( X misses Z & Y misses V ) ; :: thesis: ( X = V & Y = Z )
then A2: ( X /\ Z = [[0]] I & Y /\ V = [[0]] I ) by Th111;
thus X = X /\ (Z \/ V) by Th23, A1, Th14
.= (X /\ Z) \/ (X /\ V) by Th32
.= (X \/ Y) /\ V by A2, Th32
.= V by A1, Th14, Th23 ; :: thesis: Y = Z
thus Y = Y /\ (Z \/ V) by Th23, A1, Th14
.= (Y /\ Z) \/ (Y /\ V) by Th32
.= (X \/ Y) /\ Z by A2, Th32
.= Z by A1, Th14, Th23 ; :: thesis: verum