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