let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I st X c= Y & X c= Z & Y misses Z holds
X = EmptyMS I
let X, Y, Z be ManySortedSet of I; :: thesis: ( X c= Y & X c= Z & Y misses Z implies X = EmptyMS I )
assume A1: ( X c= Y & X c= Z ) ; :: thesis: ( not Y misses Z or X = EmptyMS I )
assume Y misses Z ; :: thesis: X = EmptyMS I
then Y (/\) Z = EmptyMS I by Th111;
hence X = EmptyMS I by A1, Th17, Th44; :: thesis: verum