let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I st X c= Y (\/) Z holds
( X (\) Y c= Z & X (\) Z c= Y )
let X, Y, Z be ManySortedSet of I; :: thesis: ( X c= Y (\/) Z implies ( X (\) Y c= Z & X (\) Z c= Y ) )
assume A1: X c= Y (\/) Z ; :: thesis: ( X (\) Y c= Z & X (\) Z c= Y )
then X (\) Y c= (Z (\/) Y) (\) Y by Th53;
then A2: X (\) Y c= Z (\) Y by Th75;
Z (\) Y c= Z by Th56;
hence X (\) Y c= Z by A2, Th13; :: thesis: X (\) Z c= Y
X (\) Z c= (Y (\/) Z) (\) Z by A1, Th53;
then A3: X (\) Z c= Y (\) Z by Th75;
Y (\) Z c= Y by Th56;
hence X (\) Z c= Y by A3, Th13; :: thesis: verum