let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I st X c= Y & Y /\ Z = [[0]] I holds
X /\ Z = [[0]] I
let X, Y, Z be ManySortedSet of I; :: thesis: ( X c= Y & Y /\ Z = [[0]] I implies X /\ Z = [[0]] I )
assume X c= Y ; :: thesis: ( not Y /\ Z = [[0]] I or X /\ Z = [[0]] I )
then X /\ Z c= Y /\ Z by Th21;
hence ( not Y /\ Z = [[0]] I or X /\ Z = [[0]] I ) by Th50; :: thesis: verum