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