let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I st X c= Y /\ Z holds
X c= Y
let X, Y, Z be ManySortedSet of I; :: thesis: ( X c= Y /\ Z implies X c= Y )
Y /\ Z c= Y by Th15;
hence ( X c= Y /\ Z implies X c= Y ) by Th13; :: thesis: verum