theorem :: GFACIRC1:7

for x, y, z being Element of BOOLEAN holds (('not' x) 'xor' y) 'xor' ('not' z) = (x 'xor' ('not' y)) 'xor' ('not' z) ;