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