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) by Th93
.= X (\+\) (Y (\+\) (X (\/) Y)) by Th95
.= (X (\+\) Y) (\+\) (X (\/) Y) by Th90 ; :: thesis: verum