let I be set ; :: thesis: for X, Y being ManySortedSet of holds
( X /\ (X /\ Y) = X /\ Y & (X /\ Y) /\ Y = X /\ Y )
let X, Y be ManySortedSet of ; :: thesis: ( X /\ (X /\ Y) = X /\ Y & (X /\ Y) /\ Y = X /\ Y )
thus X /\ (X /\ Y) = (X /\ X) /\ Y by Th35
.= X /\ Y ; :: thesis: (X /\ Y) /\ Y = X /\ Y
thus (X /\ Y) /\ Y = X /\ (Y /\ Y) by Th35
.= X /\ Y ; :: thesis: verum