take x = 0. X; :: thesis: x is positive
thus x is positive by Lm2; :: thesis: verum