let I be set ; :: thesis: for X, Y, Z, V being ManySortedSet of I st Z (\/) V = X (\/) Y & X misses Z & Y misses V holds
( X = V & Y = Z )
let X, Y, Z, V 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 = EmptyMS I & Y (/\) V = EmptyMS 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