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