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