:: deftheorem defines \false AOFA_A01:def 6 :
for S being non empty non void bool-correct BoolSignature
for A being non-empty MSAlgebra over S holds \false A = \not (\true A);