take ].(r - 1),(r + 1).[ ; :: thesis: ex g being Real st
( 0 < g & ].(r - 1),(r + 1).[ = ].(r - g),(r + g).[ )
thus ex g being Real st
( 0 < g & ].(r - 1),(r + 1).[ = ].(r - g),(r + g).[ ) ; :: thesis: verum