let n be Nat; :: thesis: ( not Necklace n, ComplRelStr () are_isomorphic or n = 0 or n = 1 or n = 4 )
assume A1: Necklace n, ComplRelStr () are_isomorphic ; :: thesis: ( n = 0 or n = 1 or n = 4 )
set S = Necklace n;
set T = ComplRelStr ();
card n = n ;
then A2: card [:n,n:] = n * n by CARD_2:46;
assume A3: ( not n = 0 & not n = 1 & not n = 4 ) ; :: thesis: contradiction
( n <= 4 implies not not n = 0 & ... & not n = 4 ) ;
then ( n = 2 or n = 3 or n > 4 ) by A3;
then A4: card the InternalRel of () = 2 * (n - 1) by Th26;
A5: ((n * n) - (2 * (n - 1))) - n <> 2 * (n - 1)
proof
A6: delta (1,(- 5),4) = ((- 5) ^2) - ((4 * 1) * 4) by QUIN_1:def 1
.= 9 ;
assume not ((n * n) - (2 * (n - 1))) - n <> 2 * (n - 1) ; :: thesis: contradiction
then ((1 * (n ^2)) + ((- 5) * n)) + 4 = 0 ;
then ( n = ((- (- 5)) - (sqrt (delta (1,(- 5),4)))) / (2 * 1) or n = ((- (- 5)) + (sqrt (delta (1,(- 5),4)))) / (2 * 1) ) by ;
then ( n = (5 - (sqrt (3 ^2))) / 2 or n = (5 + (sqrt (3 ^2))) / 2 ) by A6;
then A7: ( n = (5 - 3) / 2 or n = (5 + 3) / 2 ) by SQUARE_1:22;
per cases ( n = 1 or n = 4 ) by A7;
end;
end;
A8: id the carrier of () misses the InternalRel of ()
proof
assume not id the carrier of () misses the InternalRel of () ; :: thesis: contradiction
then consider x being object such that
A9: x in id the carrier of () and
A10: x in the InternalRel of () by XBOOLE_0:3;
consider i being Element of NAT such that
i + 1 < n and
A11: ( x = [i,(i + 1)] or x = [(i + 1),i] ) by ;
consider x1, x2 being object such that
A12: x = [x1,x2] by ;
A13: x1 = x2 by ;
per cases ( [x1,x2] = [i,(i + 1)] or [x1,x2] = [(i + 1),i] ) by ;
suppose [x1,x2] = [i,(i + 1)] ; :: thesis: contradiction
end;
suppose [x1,x2] = [(i + 1),i] ; :: thesis: contradiction
end;
end;
end;
the carrier of () = n by Th19;
then A14: card ( the InternalRel of () `) = (n * n) - (2 * (n - 1)) by ;
( the carrier of () = n & n = card n ) by Th19;
then A15: card (id the carrier of ()) = n by Th4;
card the InternalRel of () = card (( the InternalRel of () `) \ (id the carrier of ())) by Def8
.= ((n * n) - (2 * (n - 1))) - n by ;
hence contradiction by A1, A4, A5, Th16; :: thesis: verum