let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I st X c= Y holds
( X /\ Z c= Y /\ Z & Z /\ X c= Z /\ Y )
let X, Y, Z be ManySortedSet of I; :: thesis: ( X c= Y implies ( X /\ Z c= Y /\ Z & Z /\ X c= Z /\ Y ) )
assume A1: X c= Y ; :: thesis: ( X /\ Z c= Y /\ Z & Z /\ X c= Z /\ Y )
A2: X /\ Z c= Z by Th17;
X /\ Z c= X by Th17;
then X /\ Z c= Y by A1, Th15;
hence X /\ Z c= Y /\ Z by A2, Th19; :: thesis: Z /\ X c= Z /\ Y
A3: Z /\ X c= Z by Th17;
Z /\ X c= X by Th17;
then Z /\ X c= Y by A1, Th15;
hence Z /\ X c= Z /\ Y by A3, Th19; :: thesis: verum