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