theorem :: REVROT_1:2

canceled;