:: deftheorem defines VeRUM PL_AXIOM:def 10 :
VeRUM = 'not' FaLSUM;