let v be Element of M; :: thesis: ( ( v in W1 + W implies v in W1 + W9 ) & ( v in W1 + W9 implies v in W1 + W ) ) set W1W9 = { (v1 + v2) where v2, v1 is Element of M : ( v1 in W1 & v2 in W9 ) } ; set W1W = { (v1 + v2) where v2, v1 is Element of M : ( v1 in W1 & v2 in W ) } ; thus
( v in W1 + W implies v in W1 + W9 )
:: thesis: ( v in W1 + W9 implies v in W1 + W )