let p be Real; :: thesis: (exp_R . p) + (exp_R . (- p)) >= 2
A1: ( exp_R . p >= 0 & exp_R . (- p) >= 0 ) by SIN_COS:54;
2 * (sqrt ((exp_R . p) * (exp_R . (- p)))) = 2 * (sqrt (exp_R . (p + (- p)))) by Th12
.= 2 * 1 by SIN_COS:51, SIN_COS:def 23, SQUARE_1:18 ;
hence (exp_R . p) + (exp_R . (- p)) >= 2 by A1, Th1; :: thesis: verum