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