theorem :: REVROT_1:6

canceled;