theorem :: RECDEF_2:7

canceled;