let p, q, r be boolean object ; :: thesis: (p 'xor' q) 'xor' r = p 'xor' (q 'xor' r)
( q = FALSE or q = TRUE ) by Def3;
hence (p 'xor' q) 'xor' r = p 'xor' (q 'xor' r) ; :: thesis: verum