:: deftheorem defines are_twin NUMBER10:def 1 :
for r, s being Complex holds
( r,s are_twin iff |.(s - r).| = 2 );