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