let r be Real; :: thesis: ( frac r = 0 iff r is integer )

now :: thesis: ( r is Integer implies frac r = 0 )

assume r is Integer ; :: thesis: frac r = 0
then r = [\r/] by Th25;
hence frac r = 0 ; :: thesis: verum

end;

hence ( frac r = 0 iff r is integer ) ; :: thesis: verum