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