theorem :: RECDEF_2:4

canceled;