r <> 0 ;
then ( 1 - r <> 0 & 1 - r <> 1 ) by Def01;
hence 1 - r is non zero non unit Real by Def01; :: thesis: verum