let I be set ; :: thesis: for m, n being bag of I holds n = (m -' (m -' n)) + (n -' m)
let m, n be bag of I; :: thesis: n = (m -' (m -' n)) + (n -' m)
let a be object ; :: according to PBOOLE:def 10 :: thesis: ( not a in I or n . a = ((m -' (m -' n)) + (n -' m)) . a )
assume a in I ; :: thesis: n . a = ((m -' (m -' n)) + (n -' m)) . a
thus n . a = ((m . a) -' ((m . a) -' (n . a))) + ((n . a) -' (m . a)) by Th6
.= ((m . a) -' ((m -' n) . a)) + ((n . a) -' (m . a)) by PRE_POLY:def 6
.= ((m -' (m -' n)) . a) + ((n . a) -' (m . a)) by PRE_POLY:def 6
.= ((m -' (m -' n)) . a) + ((n -' m) . a) by PRE_POLY:def 6
.= ((m -' (m -' n)) + (n -' m)) . a by PRE_POLY:def 5 ; :: thesis: verum