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