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
V c= Y (\/) V by Th14;
then A3: Z c= Y (\/) V by A2, Th13;
Y c= Y (\/) V by Th14;
then X c= Y (\/) V by A1, Th13;
hence X (\/) Z c= Y (\/) V by A3, Th16; :: thesis: verum