let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I st (X (/\) Y) (\/) (X (/\) Z) = X holds
X c= Y (\/) Z
let X, Y, Z be ManySortedSet of I; :: thesis: ( (X (/\) Y) (\/) (X (/\) Z) = X implies X c= Y (\/) Z )
assume (X (/\) Y) (\/) (X (/\) Z) = X ; :: thesis: X c= Y (\/) Z
then X = X (/\) (Y (\/) Z) by Th32;
hence X c= Y (\/) Z by Th15; :: thesis: verum