let I be set ; :: thesis: for X, Y, Z, V being ManySortedSet of I st X c= Y & Z c= V holds
X \ V c= Y \ Z
let X, Y, Z, V be ManySortedSet of I; :: thesis: ( X c= Y & Z c= V implies X \ V c= Y \ Z )
assume ( X c= Y & Z c= V ) ; :: thesis: X \ V c= Y \ Z
then ( X \ V c= Y \ V & Y \ V c= Y \ Z ) by Th59, Th60;
hence X \ V c= Y \ Z by Th15; :: thesis: verum