let n be Nat; :: thesis: for i, j being Nat holds

( not [i,j] in the InternalRel of (Necklace n) or i = j + 1 or j = i + 1 )

let i, j be Nat; :: thesis: ( not [i,j] in the InternalRel of (Necklace n) or i = j + 1 or j = i + 1 )

assume [i,j] in the InternalRel of (Necklace n) ; :: thesis: ( i = j + 1 or j = i + 1 )

then [i,j] in { [k,(k + 1)] where k is Element of NAT : k + 1 < n } \/ { [(l + 1),l] where l is Element of NAT : l + 1 < n } by Th17;

then A1: ( [i,j] in { [k,(k + 1)] where k is Element of NAT : k + 1 < n } or [i,j] in { [(k + 1),k] where k is Element of NAT : k + 1 < n } ) by XBOOLE_0:def 3;

( i + 1 = j or j + 1 = i )

( not [i,j] in the InternalRel of (Necklace n) or i = j + 1 or j = i + 1 )

let i, j be Nat; :: thesis: ( not [i,j] in the InternalRel of (Necklace n) or i = j + 1 or j = i + 1 )

assume [i,j] in the InternalRel of (Necklace n) ; :: thesis: ( i = j + 1 or j = i + 1 )

then [i,j] in { [k,(k + 1)] where k is Element of NAT : k + 1 < n } \/ { [(l + 1),l] where l is Element of NAT : l + 1 < n } by Th17;

then A1: ( [i,j] in { [k,(k + 1)] where k is Element of NAT : k + 1 < n } or [i,j] in { [(k + 1),k] where k is Element of NAT : k + 1 < n } ) by XBOOLE_0:def 3;

( i + 1 = j or j + 1 = i )

proof
end;

hence
( i = j + 1 or j = i + 1 )
; :: thesis: verumper cases
( ex k being Element of NAT st

( [i,j] = [k,(k + 1)] & k + 1 < n ) or ex k being Element of NAT st

( [i,j] = [(k + 1),k] & k + 1 < n ) ) by A1;

( [i,j] = [k,(k + 1)] & k + 1 < n ) or ex k being Element of NAT st

( [i,j] = [(k + 1),k] & k + 1 < n ) ) by A1;

end;