let I be set ; :: thesis: for X, A, Y being ManySortedSet of I st X c= A holds
X \ Y c= A
let X, A, Y be ManySortedSet of I; :: thesis: ( X c= A implies X \ Y c= A )
assume A1: X c= A ; :: thesis: X \ Y c= A
let i be set ; :: according to PBOOLE:def 2 :: 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 by A1, PBOOLE:def 2;
then (X . i) \ (Y . i) c= A . i by XBOOLE_1:109;
hence (X \ Y) . i c= A . i by A2, PBOOLE:def 6; :: thesis: verum