let n be Nat; for x being set holds
( x in the InternalRel of (Necklace n) iff ex i being Element of NAT st
( i + 1 < n & ( x = [i,(i + 1)] or x = [(i + 1),i] ) ) )
let x be set ; ( x in the InternalRel of (Necklace n) iff ex i being Element of NAT st
( i + 1 < n & ( x = [i,(i + 1)] or x = [(i + 1),i] ) ) )
thus
( x in the InternalRel of (Necklace n) implies ex i being Element of NAT st
( i + 1 < n & ( x = [i,(i + 1)] or x = [(i + 1),i] ) ) )
( ex i being Element of NAT st
( i + 1 < n & ( x = [i,(i + 1)] or x = [(i + 1),i] ) ) implies x in the InternalRel of (Necklace n) )proof
assume
x in the
InternalRel of
(Necklace n)
;
ex i being Element of NAT st
( i + 1 < n & ( x = [i,(i + 1)] or x = [(i + 1),i] ) )
then
x in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } \/ { [(i + 1),i] where i is Element of NAT : i + 1 < n }
by Th17;
then
(
x in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } or
x in { [(i + 1),i] where i is Element of NAT : i + 1 < n } )
by XBOOLE_0:def 3;
then
( ex
i being
Element of
NAT st
(
x = [i,(i + 1)] &
i + 1
< n ) or ex
i being
Element of
NAT st
(
x = [(i + 1),i] &
i + 1
< n ) )
;
hence
ex
i being
Element of
NAT st
(
i + 1
< n & (
x = [i,(i + 1)] or
x = [(i + 1),i] ) )
;
verum
end;
thus
( ex i being Element of NAT st
( i + 1 < n & ( x = [i,(i + 1)] or x = [(i + 1),i] ) ) implies x in the InternalRel of (Necklace n) )
verum