theorem :: SUPINF_2:4

canceled;