let r be real number ; :: thesis: ( r is geq_than_1 implies r is positive )
assume 1 <= r ; :: according to LPSPACE2:def 1 :: thesis: r is positive
hence r is positive ; :: thesis: verum