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

now

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

end;

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