theorem Th33: :: MODAL_1:38

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