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