let a be non zero Element of N_Real; :: thesis: not a is empty
0. N_Real = 0 ;
hence not a is empty ; :: thesis: verum