:: deftheorem defines FaLSUM PL_AXIOM:def 4 :
FaLSUM = <*0*>;