let r be Real; :: 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 )
A2: r <= [/r\] by Def7;
r - 1 < [\r/] by Def6;
then (r - 1) + 1 < [\r/] + 1 by XREAL_1:6;
then 0 - 1 < ([\r/] + 1) - 1 by A1, XREAL_1:9;
then [\r/] >= 0 by Th8;
hence ( [/r\] >= 0 & [\r/] >= 0 & [/r\] is Element of NAT & [\r/] is Element of NAT ) by A1, A2, Th3; :: thesis: verum