let r be real number ; :: thesis: ( r >= 0 implies ( [/r\] >= 0 & [\r/] >= 0 & [/r\] is Element of NAT & [\r/] is Element of NAT ) )
assume A1: r >= 0 ; :: thesis: ( [/r\] >= 0 & [\r/] >= 0 & [/r\] is Element of NAT & [\r/] is Element of NAT )
r - 1 < [\r/] by Def4;
then (r - 1) + 1 < [\r/] + 1 by XREAL_1:8;
then 0 - 1 < ([\r/] + 1) - 1 by A1, XREAL_1:11;
then A2: [\r/] >= 0 by Th21;
r <= [/r\] by Def5;
hence ( [/r\] >= 0 & [\r/] >= 0 & [/r\] is Element of NAT & [\r/] is Element of NAT ) by A1, A2, Th16; :: thesis: verum