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