let I be set ; :: thesis: for X, A, Y being ManySortedSet of st X c= A & Y c= A holds
X \+\ Y c= A
let X, A, Y be ManySortedSet of ; :: thesis: ( X c= A & Y c= A implies X \+\ Y c= A )
assume A1: ( X c= A & Y c= A ) ; :: thesis: X \+\ Y c= A
let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or (X \+\ Y) . i c= A . i )
assume A2: i in I ; :: thesis: (X \+\ Y) . i c= A . i
then ( X . i c= A . i & Y . i c= A . i ) by A1, PBOOLE:def 5;
then (X . i) \+\ (Y . i) c= A . i by XBOOLE_1:110;
then (X . i) \+\ (Y . i) in bool (A . i) ;
then (X \+\ Y) . i in bool (A . i) by A2, PBOOLE:4;
hence (X \+\ Y) . i c= A . i ; :: thesis: verum