theorem Th31: :: MODAL_1:36

for A being MP-wff holds
( not card (dom A) = 1 or A = VERUM or ex p being MP-variable st A = @ p )