take 0 ; :: thesis: 0 is real
thus 0 in REAL by NUMBERS:19; :: according to XREAL_0:def 1 :: thesis: verum