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