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