let I be set ; :: thesis: for X, Z, Y being ManySortedSet of I st X c= Z & Y c= Z holds
X \/ Y c= Z
let X, Z, Y be ManySortedSet of I; :: thesis: ( X c= Z & Y c= Z implies X \/ Y c= Z )
assume A1: ( X c= Z & Y c= Z ) ; :: thesis: X \/ Y c= Z
let i be set ; :: according to PBOOLE:def 2 :: thesis: ( i in I implies (X \/ Y) . i c= Z . i )
assume A2: i in I ; :: thesis: (X \/ Y) . i c= Z . i
then ( X . i c= Z . i & Y . i c= Z . i ) by A1, Def5;
then (X . i) \/ (Y . i) c= Z . i by XBOOLE_1:8;
hence (X \/ Y) . i c= Z . i by A2, Def7; :: thesis: verum