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 )
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 A1;
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
A2: [i,j] = [k,(k + 1)] and
k + 1 < n ;
i = k by A2, XTUPLE_0:1;
hence ( i + 1 = j or j + 1 = i ) by A2, XTUPLE_0:1; :: 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
A3: [i,j] = [(k + 1),k] and
k + 1 < n ;
i = k + 1 by A3, XTUPLE_0:1;
hence ( i + 1 = j or j + 1 = i ) by A3, XTUPLE_0:1; :: thesis: verum
end;
end;
end;
hence ( i = j + 1 or j = i + 1 ) ; :: thesis: verum