let x be set ; :: according to NECKLACE:def 5 :: thesis: ( x in the carrier of () implies not [x,x] in the InternalRel of () )
set A = Necklace n;
assume x in the carrier of () ; :: thesis: not [x,x] in the InternalRel of ()
A1: the InternalRel of () = { [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 () ; :: 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 ;
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 ;
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 ;
hence contradiction ; :: thesis: verum
end;
end;