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