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