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