let I be set ; :: thesis: for m, n, x, y being bag of I st n = (m -' x) + y holds
( m -' n divides x & n -' m divides y )
let m, n, x, y be bag of I; :: thesis: ( n = (m -' x) + y implies ( m -' n divides x & n -' m divides y ) )
assume Z0: n = (m -' x) + y ; :: thesis: ( m -' n divides x & n -' m divides y )
thus m -' n divides x :: thesis: n -' m divides y

proof

let a be object ; :: according to PRE_POLY:def 11 :: thesis: (m -' n) . a <= x . a
n . a = ((m -' x) . a) + (y . a) by Z0, PRE_POLY:def 5
.= ((m . a) -' (x . a)) + (y . a) by PRE_POLY:def 6 ;
then (m . a) -' (n . a) <= x . a by Th5;
hence (m -' n) . a <= x . a by PRE_POLY:def 6; :: thesis: verum

end;

let a be object ; :: according to PRE_POLY:def 11 :: thesis: (n -' m) . a <= y . a
n . a = ((m -' x) . a) + (y . a) by Z0, PRE_POLY:def 5
.= ((m . a) -' (x . a)) + (y . a) by PRE_POLY:def 6 ;
then (n . a) -' (m . a) <= y . a by Th5;
hence (n -' m) . a <= y . a by PRE_POLY:def 6; :: thesis: verum