let x be set ; :: according to NECKLACE:def 5 :: thesis: ( x in the carrier of (Necklace n) implies not [x,x] in the InternalRel of (Necklace n) )
set A = Necklace n;
assume x in the carrier of (Necklace n) ; :: thesis: not [x,x] in the InternalRel of (Necklace n)
A1: the InternalRel of (Necklace n) = { [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;
assume A2: [x,x] in the InternalRel of (Necklace n) ; :: thesis: contradiction
per cases ( [x,x] in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } or [x,x] in { [(i + 1),i] where i is Element of NAT : i + 1 < n } ) by A2, A1, XBOOLE_0:def 3;
suppose [x,x] in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } ; :: thesis: contradiction
then consider i being Element of NAT such that
A3: [x,x] = [i,(i + 1)] and
i + 1 < n ;
( x = i & x = i + 1 ) by A3, XTUPLE_0:1;
hence contradiction ; :: thesis: verum
end;
suppose [x,x] in { [(i + 1),i] where i is Element of NAT : i + 1 < n } ; :: thesis: contradiction
then consider i being Element of NAT such that
A4: [x,x] = [(i + 1),i] and
i + 1 < n ;
( x = i + 1 & x = i ) by A4, XTUPLE_0:1;
hence contradiction ; :: thesis: verum
end;
end;