let I be set ; for m, n, x, y being bag of I st x divides m & n = (m -' x) + y holds
x -' (m -' n) = y -' (n -' m)
let m, n, x, y be bag of I; ( x divides m & n = (m -' x) + y implies x -' (m -' n) = y -' (n -' m) )
assume Z0:
x divides m
; ( not n = (m -' x) + y or x -' (m -' n) = y -' (n -' m) )
assume Z1:
n = (m -' x) + y
; x -' (m -' n) = y -' (n -' m)
let a be object ; PBOOLE:def 10 ( not a in I or (x -' (m -' n)) . a = (y -' (n -' m)) . a )
assume
a in I
; (x -' (m -' n)) . a = (y -' (n -' m)) . a
A1:
( n . a = ((m -' x) . a) + (y . a) & ((m -' x) . a) + (y . a) = ((m . a) -' (x . a)) + (y . a) & x . a <= m . a )
by Z0, Z1, PRE_POLY:def 5, PRE_POLY:def 6, PRE_POLY:def 11;
thus (x -' (m -' n)) . a =
(x . a) -' ((m -' n) . a)
by PRE_POLY:def 6
.=
(x . a) -' ((m . a) -' (n . a))
by PRE_POLY:def 6
.=
(y . a) -' ((n . a) -' (m . a))
by A1, Th5A
.=
(y . a) -' ((n -' m) . a)
by PRE_POLY:def 6
.=
(y -' (n -' m)) . a
by PRE_POLY:def 6
; verum