let S be non empty non void bool-correct 4,1 integer BoolSignature ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for T being b₁,S -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 )
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for T being X,S -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 )
let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S; :: thesis: 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 )
let C be bool-correct 4,1 integer image of T; :: thesis: for a being Element of C, the bool-sort of S
for x being boolean object holds
( \not a = 'not' x iff a = x )
let a be Element of C, the bool-sort of S; :: thesis: for x being boolean object holds
( \not a = 'not' x iff a = x )
a in the Sorts of C . the bool-sort of S ;
then a in BOOLEAN by AOFA_A00:def 32;
then reconsider b = a as boolean object ;
let x be boolean object ; :: thesis: ( \not a = 'not' x iff a = x )

hereby :: thesis: ( a = x implies \not a = 'not' x )

assume \not a = 'not' x ; :: thesis: a = x
then 'not' b = 'not' x by AOFA_A00:def 32;
hence a = x ; :: thesis: verum

end;

assume a = x ; :: thesis: \not a = 'not' x
hence \not a = 'not' x by AOFA_A00:def 32; :: thesis: verum