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