let r be Real; :: thesis: ( uReal . r == 0_No implies r = 0 )
assume uReal . r == 0_No ; :: thesis: r = 0
then ( 0 <= r & r <= 0 ) by SURREALN:51, SURREALN:47;
hence r = 0 ; :: thesis: verum