let I be set ; :: thesis: for X, Y, Z, V being ManySortedSet of I st X c= Y & Z c= V holds
X (\) V c= Y (\) Z
let X, Y, Z, V be ManySortedSet of I; :: thesis: ( X c= Y & Z c= V implies X (\) V c= Y (\) Z )
assume ( X c= Y & Z c= V ) ; :: thesis: X (\) V c= Y (\) Z
then ( X (\) V c= Y (\) V & Y (\) V c= Y (\) Z ) by Th53, Th54;
hence X (\) V c= Y (\) Z by Th13; :: thesis: verum