let r, s be Real; :: thesis: ex i being Integer st
( frac (r - s) = ((frac r) - (frac s)) + i & ( i = 0 or i = 1 ) )
( frac (r - s) = ((frac r) - (frac s)) + Q or frac (r - s) = ((frac r) - (frac s)) + 1 ) by Th2, Th3;
hence ex i being Integer st
( frac (r - s) = ((frac r) - (frac s)) + i & ( i = 0 or i = 1 ) ) ; :: thesis: verum