let I be set ; 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; ( X c= Y & Z c= V implies X \/ Z c= Y \/ V )
assume that
A1:
X c= Y
and
A2:
Z c= V
; X \/ Z c= Y \/ V
V c= Y \/ V
by Th16;
then A3:
Z c= Y \/ V
by A2, Th15;
Y c= Y \/ V
by Th16;
then
X c= Y \/ V
by A1, Th15;
hence
X \/ Z c= Y \/ V
by A3, Th18; verum