let S be non empty non void bool-correct 4,1 integer BoolSignature ; :: thesis: for X being V3() ManySortedSet of the carrier of S
for T being non-empty b₁,S -terms vf-free integer VarMSAlgebra over S
for C being bool-correct 4,1 integer image of T holds \false C = FALSE
let X be V3() ManySortedSet of the carrier of S; :: thesis: for T being non-empty X,S -terms vf-free integer VarMSAlgebra over S
for C being bool-correct 4,1 integer image of T holds \false C = FALSE
let T be non-empty X,S -terms vf-free integer VarMSAlgebra over S; :: thesis: for C being bool-correct 4,1 integer image of T holds \false C = FALSE
let C be bool-correct 4,1 integer image of T; :: thesis: \false C = FALSE
\true C = TRUE by AOFA_A00:def 32;
hence \false C = 'not' TRUE by AOFA_A00:def 32
.= FALSE ;
:: thesis: verum