theorem :: BKMODEL1:45

symmetric_3 (1,1,1,0,0,0) = 1. (F_Real,3) by PASCAL:def 3, ANPROJ_9:1;