let a, b, c be Point of CLS; :: thesis: ( [a,b,c] in RR iff ( ( a = b or b = c or c = a ) & a in Z & b in Z & c in Z ) )
thus ( [a,b,c] in RR implies ( ( a = b or b = c or c = a ) & a in Z & b in Z & c in Z ) ) :: thesis: ( ( a = b or b = c or c = a ) & a in Z & b in Z & c in Z implies [a,b,c] in RR )

proof

assume [a,b,c] in RR ; :: thesis: ( ( a = b or b = c or c = a ) & a in Z & b in Z & c in Z )
then consider i, j, k being Element of NAT such that
A1: [a,b,c] = [i,j,k] and
A2: ( i = j or j = k or k = i ) and
i in Z and
j in Z and
k in Z ;
( a = i & b = j ) by A1, XTUPLE_0:3;
hence ( ( a = b or b = c or c = a ) & a in Z & b in Z & c in Z ) by A1, A2, XTUPLE_0:3; :: thesis: verum

end;

thus ( ( a = b or b = c or c = a ) & a in Z & b in Z & c in Z implies [a,b,c] in RR ) ; :: thesis: verum