let th be real number ; :: thesis: exp_R . th > 0

A1: now

per cases ( th = 0 or th <> 0 ) ;

suppose A2: th = 0 ; :: thesis: exp_R . th > 0

thus exp_R . th > 0 by A2, Lm12; :: thesis: verum

end;

suppose A3: th <> 0 ; :: thesis: exp_R . th > 0

A4: now

per cases ( th < 0 or th > 0 ) by A3;

suppose A5: th < 0 ; :: thesis: exp_R . th > 0

thus exp_R . th > 0 by A5, Th58; :: thesis: verum

end;

suppose A6: th > 0 ; :: thesis: exp_R . th > 0

thus exp_R . th > 0 by A6, Th57; :: thesis: verum

end;

end;

end;

thus exp_R . th > 0 by A4; :: thesis: verum

end;

end;

end;

thus exp_R . th > 0 by A1; :: thesis: verum