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