let th be Real; :: thesis:

now :: thesis:

per cases ;

suppose th = 0 ; :: thesis:

hence exp_R . th > 0 by Lm11; :: thesis:

end;

suppose A1: th <> 0 ; :: thesis:

now :: thesis:

per cases by A1;

suppose th < 0 ; :: thesis:

hence exp_R . th > 0 by Th52; :: thesis:

end;

suppose th > 0 ; :: thesis:

hence exp_R . th > 0 by Th51; :: thesis:

end;

end;

end;

hence exp_R . th > 0 ; :: thesis:

end;

end;

end;

hence exp_R . th > 0 ; :: thesis: