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