reconsider z = 0 as ext-real number ;
take z ; :: thesis: z is zero
thus z = 0 ; :: according to XXREAL_0:def 8 :: thesis: verum