let a, b, c be Point of CLS; ( [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 ) )
( ( 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
;
( ( 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;
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 )
; verum