theorem Th34: :: MODAL_1:39

for A being MP-wff holds card (dom A) < card (dom ((#) A))