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