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 A1: [i,j] in the InternalRel of (Necklace n) ; :: thesis: ( i = j + 1 or j = i + 1 )
[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 A1, Th19;
then A2: ( [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

per 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 A2;

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

then consider k being Nat such that
A3: [i,j] = [k,(k + 1)] and
k + 1 < n ;
( i = k & j = k + 1 ) by A3, ZFMISC_1:33;
hence ( i + 1 = j or j + 1 = i ) ; :: thesis: verum

end;

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

then consider k being Nat such that
A4: [i,j] = [(k + 1),k] and
k + 1 < n ;
( i = k + 1 & j = k ) by A4, ZFMISC_1:33;
hence ( i + 1 = j or j + 1 = i ) ; :: thesis: verum

end;

end;

end;

hence ( i = j + 1 or j = i + 1 ) ; :: thesis: verum