theorem :: RECDEF_2:1

canceled;