:: deftheorem defines consistent PETERSON:def 1 :
for A being Values_with_TF holds
( A is consistent iff the True of A <> the False of A );