let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I st X c= Y (/\) Z holds
X c= Y
let X, Y, Z be ManySortedSet of I; :: thesis: ( X c= Y (/\) Z implies X c= Y )
Y (/\) Z c= Y by Th15;
hence ( X c= Y (/\) Z implies X c= Y ) by Th13; :: thesis: verum