let r, s be Real; :: thesis: ( r <= s implies ( r,s are_twin iff s - r = 2 ) )
assume r <= s ; :: thesis: ( r,s are_twin iff s - r = 2 )
then s - r >= r - r by XREAL_1:7;
hence ( r,s are_twin iff s - r = 2 ) by ABSVALUE:def 1; :: thesis: verum