let n be Nat; :: thesis: ( not Necklace n, ComplRelStr (Necklace n) are_isomorphic or n = 0 or n = 1 or n = 4 )

assume A1: Necklace n, ComplRelStr (Necklace n) are_isomorphic ; :: thesis: ( n = 0 or n = 1 or n = 4 )

set S = Necklace n;

set T = ComplRelStr (Necklace n);

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 (Necklace n) = 2 * (n - 1) by Th26;

A5: ((n * n) - (2 * (n - 1))) - n <> 2 * (n - 1)

then A14: card ( the InternalRel of (Necklace n) `) = (n * n) - (2 * (n - 1)) by A4, A2, CARD_2:44;

( the carrier of (Necklace n) = n & n = card n ) by Th19;

then A15: card (id the carrier of (Necklace n)) = n by Th4;

card the InternalRel of (ComplRelStr (Necklace n)) = card (( the InternalRel of (Necklace n) `) \ (id the carrier of (Necklace n))) by Def8

.= ((n * n) - (2 * (n - 1))) - n by A14, A15, A8, CARD_2:44, XBOOLE_1:86 ;

hence contradiction by A1, A4, A5, Th16; :: thesis: verum

assume A1: Necklace n, ComplRelStr (Necklace n) are_isomorphic ; :: thesis: ( n = 0 or n = 1 or n = 4 )

set S = Necklace n;

set T = ComplRelStr (Necklace n);

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 (Necklace n) = 2 * (n - 1) by Th26;

A5: ((n * n) - (2 * (n - 1))) - n <> 2 * (n - 1)

proof

A8:
id the carrier of (Necklace n) misses the InternalRel of (Necklace n)
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 A6, QUIN_1:15;

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;

end;.= 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 A6, QUIN_1:15;

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;

proof

the carrier of (Necklace n) = n
by Th19;
assume
not id the carrier of (Necklace n) misses the InternalRel of (Necklace n)
; :: thesis: contradiction

then consider x being object such that

A9: x in id the carrier of (Necklace n) and

A10: x in the InternalRel of (Necklace n) 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 A10, Th18;

consider x1, x2 being object such that

A12: x = [x1,x2] by A9, RELAT_1:def 1;

A13: x1 = x2 by A9, A12, RELAT_1:def 10;

end;then consider x being object such that

A9: x in id the carrier of (Necklace n) and

A10: x in the InternalRel of (Necklace n) 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 A10, Th18;

consider x1, x2 being object such that

A12: x = [x1,x2] by A9, RELAT_1:def 1;

A13: x1 = x2 by A9, A12, RELAT_1:def 10;

then A14: card ( the InternalRel of (Necklace n) `) = (n * n) - (2 * (n - 1)) by A4, A2, CARD_2:44;

( the carrier of (Necklace n) = n & n = card n ) by Th19;

then A15: card (id the carrier of (Necklace n)) = n by Th4;

card the InternalRel of (ComplRelStr (Necklace n)) = card (( the InternalRel of (Necklace n) `) \ (id the carrier of (Necklace n))) by Def8

.= ((n * n) - (2 * (n - 1))) - n by A14, A15, A8, CARD_2:44, XBOOLE_1:86 ;

hence contradiction by A1, A4, A5, Th16; :: thesis: verum