let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I st X c= Y \/ Z & X /\ Z = [[0]] I holds
X c= Y
let X, Y, Z be ManySortedSet of I; :: thesis: ( X c= Y \/ Z & X /\ Z = [[0]] I implies X c= Y )
assume that
A1: X c= Y \/ Z and
A2: X /\ Z = [[0]] I ; :: thesis: X c= Y
X /\ (Y \/ Z) = X by A1, Th25;
then (Y /\ X) \/ ([[0]] I) = X by A2, Th38;
then Y /\ X = X by Th53;
hence X c= Y by Th17; :: thesis: verum