theorem Th33: :: AOFA_A01:33

for S being non empty non void bool-correct 4,1 integer BoolSignature
for X being non-empty ManySortedSet of the carrier of S
for T being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S
for C being bool-correct 4,1 integer image of T
for a being Element of C, the bool-sort of S
for x being boolean object holds
( \not a = 'not' x iff a = x )