reconsider z = 0 as ExtReal ;
take z ; :: thesis: z is zero
thus z = 0 ; :: according to ORDINAL1:def 14 :: thesis: verum