theorem Th32: :: MODAL_1:37

for A being MP-wff holds
( not card (dom A) >= 2 or ex B being MP-wff st
( A = 'not' B or A = (#) B ) or ex B, C being MP-wff st A = B '&' C )