let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I st X c= Y (\/) Z & X (/\) Z = EmptyMS I holds
X c= Y
let X, Y, Z be ManySortedSet of I; :: thesis: ( X c= Y (\/) Z & X (/\) Z = EmptyMS I implies X c= Y )
assume that
A1: X c= Y (\/) Z and
A2: X (/\) Z = EmptyMS I ; :: thesis: X c= Y
X (/\) (Y (\/) Z) = X by A1, Th23;
then (Y (/\) X) (\/) (EmptyMS I) = X by A2, Th32;
then Y (/\) X = X by Th22, Th43;
hence X c= Y by Th15; :: thesis: verum