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