theorem Th6: :: NUMBER10:6
for r, s being Real st r <= s holds
( r,s are_twin iff s - r = 2 )