:: deftheorem defines \or AOFA_A00:def 35 :
for S being non empty non void bool-correct BoolSignature
for B being non-empty MSAlgebra over S
for p, q being Element of B, the bool-sort of S holds p \or q = \not ((\not p) \and (\not q));