set N4 = Necklace 4;

set cN4 = the carrier of (Necklace 4);

set CmpN4 = ComplRelStr (Necklace 4);

A1: the carrier of (Necklace 4) = {0,1,2,3} by NECKLACE:1, NECKLACE:20;

thus the InternalRel of (ComplRelStr (Necklace 4)) c= {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} :: according to XBOOLE_0:def 10 :: thesis: {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} c= the InternalRel of (ComplRelStr (Necklace 4))

assume A8: a in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} ; :: thesis: a in the InternalRel of (ComplRelStr (Necklace 4))

set cN4 = the carrier of (Necklace 4);

set CmpN4 = ComplRelStr (Necklace 4);

A1: the carrier of (Necklace 4) = {0,1,2,3} by NECKLACE:1, NECKLACE:20;

thus the InternalRel of (ComplRelStr (Necklace 4)) c= {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} :: according to XBOOLE_0:def 10 :: thesis: {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} c= the InternalRel of (ComplRelStr (Necklace 4))

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} or a in the InternalRel of (ComplRelStr (Necklace 4)) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the InternalRel of (ComplRelStr (Necklace 4)) or x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} )

assume x in the InternalRel of (ComplRelStr (Necklace 4)) ; :: thesis: x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]}

then A2: x in ( the InternalRel of (Necklace 4) `) \ (id the carrier of (Necklace 4)) by NECKLACE:def 8;

then A3: not x in id the carrier of (Necklace 4) by XBOOLE_0:def 5;

x in the InternalRel of (Necklace 4) ` by A2, XBOOLE_0:def 5;

then A4: x in [: the carrier of (Necklace 4), the carrier of (Necklace 4):] \ the InternalRel of (Necklace 4) by SUBSET_1:def 4;

consider a1, b1 being object such that

A5: a1 in the carrier of (Necklace 4) and

A6: b1 in the carrier of (Necklace 4) and

A7: x = [a1,b1] by A2, ZFMISC_1:def 2;

end;assume x in the InternalRel of (ComplRelStr (Necklace 4)) ; :: thesis: x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]}

then A2: x in ( the InternalRel of (Necklace 4) `) \ (id the carrier of (Necklace 4)) by NECKLACE:def 8;

then A3: not x in id the carrier of (Necklace 4) by XBOOLE_0:def 5;

x in the InternalRel of (Necklace 4) ` by A2, XBOOLE_0:def 5;

then A4: x in [: the carrier of (Necklace 4), the carrier of (Necklace 4):] \ the InternalRel of (Necklace 4) by SUBSET_1:def 4;

consider a1, b1 being object such that

A5: a1 in the carrier of (Necklace 4) and

A6: b1 in the carrier of (Necklace 4) and

A7: x = [a1,b1] by A2, ZFMISC_1:def 2;

per cases
( ( a1 = 0 & b1 = 0 ) or ( a1 = 0 & b1 = 1 ) or ( a1 = 0 & b1 = 2 ) or ( a1 = 0 & b1 = 3 ) or ( a1 = 1 & b1 = 0 ) or ( a1 = 2 & b1 = 0 ) or ( a1 = 3 & b1 = 0 ) or ( a1 = 1 & b1 = 1 ) or ( a1 = 1 & b1 = 2 ) or ( a1 = 1 & b1 = 3 ) or ( a1 = 2 & b1 = 2 ) or ( a1 = 2 & b1 = 1 ) or ( a1 = 2 & b1 = 3 ) or ( a1 = 3 & b1 = 3 ) or ( a1 = 3 & b1 = 1 ) or ( a1 = 3 & b1 = 2 ) )
by A1, A5, A6, ENUMSET1:def 2;

end;

suppose
( a1 = 0 & b1 = 1 )
; :: thesis: x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]}

then
x in the InternalRel of (Necklace 4)
by A7, ENUMSET1:def 4, NECKLA_2:2;

hence x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} by A4, XBOOLE_0:def 5; :: thesis: verum

end;hence x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} by A4, XBOOLE_0:def 5; :: thesis: verum

suppose
( a1 = 1 & b1 = 0 )
; :: thesis: x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]}

then
x in the InternalRel of (Necklace 4)
by A7, ENUMSET1:def 4, NECKLA_2:2;

hence x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} by A4, XBOOLE_0:def 5; :: thesis: verum

end;hence x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} by A4, XBOOLE_0:def 5; :: thesis: verum

suppose
( a1 = 1 & b1 = 2 )
; :: thesis: x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]}

then
x in the InternalRel of (Necklace 4)
by A7, ENUMSET1:def 4, NECKLA_2:2;

hence x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} by A4, XBOOLE_0:def 5; :: thesis: verum

end;hence x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} by A4, XBOOLE_0:def 5; :: thesis: verum

suppose
( a1 = 2 & b1 = 1 )
; :: thesis: x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]}

then
x in the InternalRel of (Necklace 4)
by A7, ENUMSET1:def 4, NECKLA_2:2;

hence x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} by A4, XBOOLE_0:def 5; :: thesis: verum

end;

hence x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} by A4, XBOOLE_0:def 5; :: thesis: verum

suppose
( a1 = 2 & b1 = 3 )
; :: thesis: x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]}

then
x in the InternalRel of (Necklace 4)
by A7, ENUMSET1:def 4, NECKLA_2:2;

hence x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} by A4, XBOOLE_0:def 5; :: thesis: verum

end;

hence x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} by A4, XBOOLE_0:def 5; :: thesis: verum

assume A8: a in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} ; :: thesis: a in the InternalRel of (ComplRelStr (Necklace 4))

per cases
( a = [0,2] or a = [2,0] or a = [0,3] or a = [3,0] or a = [1,3] or a = [3,1] )
by A8, ENUMSET1:def 4;

end;

suppose A9:
a = [0,2]
; :: thesis: a in the InternalRel of (ComplRelStr (Necklace 4))

A10:
not a in the InternalRel of (Necklace 4)

then a in [: the carrier of (Necklace 4), the carrier of (Necklace 4):] by A9, ZFMISC_1:87;

then a in [: the carrier of (Necklace 4), the carrier of (Necklace 4):] \ the InternalRel of (Necklace 4) by A10, XBOOLE_0:def 5;

then A12: a in the InternalRel of (Necklace 4) ` by SUBSET_1:def 4;

not a in id the carrier of (Necklace 4) by A9, RELAT_1:def 10;

then a in ( the InternalRel of (Necklace 4) `) \ (id the carrier of (Necklace 4)) by A12, XBOOLE_0:def 5;

hence a in the InternalRel of (ComplRelStr (Necklace 4)) by NECKLACE:def 8; :: thesis: verum

end;proof

( 0 in the carrier of (Necklace 4) & 2 in the carrier of (Necklace 4) )
by A1, ENUMSET1:def 2;
assume A11:
a in the InternalRel of (Necklace 4)
; :: thesis: contradiction

end;per cases
( a = [0,1] or a = [1,0] or a = [1,2] or a = [2,1] or a = [2,3] or a = [3,2] )
by A11, ENUMSET1:def 4, NECKLA_2:2;

end;

then a in [: the carrier of (Necklace 4), the carrier of (Necklace 4):] by A9, ZFMISC_1:87;

then a in [: the carrier of (Necklace 4), the carrier of (Necklace 4):] \ the InternalRel of (Necklace 4) by A10, XBOOLE_0:def 5;

then A12: a in the InternalRel of (Necklace 4) ` by SUBSET_1:def 4;

not a in id the carrier of (Necklace 4) by A9, RELAT_1:def 10;

then a in ( the InternalRel of (Necklace 4) `) \ (id the carrier of (Necklace 4)) by A12, XBOOLE_0:def 5;

hence a in the InternalRel of (ComplRelStr (Necklace 4)) by NECKLACE:def 8; :: thesis: verum

suppose A13:
a = [2,0]
; :: thesis: a in the InternalRel of (ComplRelStr (Necklace 4))

A14:
not a in the InternalRel of (Necklace 4)

then a in [: the carrier of (Necklace 4), the carrier of (Necklace 4):] by A13, ZFMISC_1:87;

then a in [: the carrier of (Necklace 4), the carrier of (Necklace 4):] \ the InternalRel of (Necklace 4) by A14, XBOOLE_0:def 5;

then A16: a in the InternalRel of (Necklace 4) ` by SUBSET_1:def 4;

not a in id the carrier of (Necklace 4) by A13, RELAT_1:def 10;

then a in ( the InternalRel of (Necklace 4) `) \ (id the carrier of (Necklace 4)) by A16, XBOOLE_0:def 5;

hence a in the InternalRel of (ComplRelStr (Necklace 4)) by NECKLACE:def 8; :: thesis: verum

end;proof

( 0 in the carrier of (Necklace 4) & 2 in the carrier of (Necklace 4) )
by A1, ENUMSET1:def 2;
assume A15:
a in the InternalRel of (Necklace 4)
; :: thesis: contradiction

end;per cases
( a = [0,1] or a = [1,0] or a = [1,2] or a = [2,1] or a = [2,3] or a = [3,2] )
by A15, ENUMSET1:def 4, NECKLA_2:2;

end;

then a in [: the carrier of (Necklace 4), the carrier of (Necklace 4):] by A13, ZFMISC_1:87;

then a in [: the carrier of (Necklace 4), the carrier of (Necklace 4):] \ the InternalRel of (Necklace 4) by A14, XBOOLE_0:def 5;

then A16: a in the InternalRel of (Necklace 4) ` by SUBSET_1:def 4;

not a in id the carrier of (Necklace 4) by A13, RELAT_1:def 10;

then a in ( the InternalRel of (Necklace 4) `) \ (id the carrier of (Necklace 4)) by A16, XBOOLE_0:def 5;

hence a in the InternalRel of (ComplRelStr (Necklace 4)) by NECKLACE:def 8; :: thesis: verum

suppose A17:
a = [0,3]
; :: thesis: a in the InternalRel of (ComplRelStr (Necklace 4))

A18:
not a in the InternalRel of (Necklace 4)

then a in [: the carrier of (Necklace 4), the carrier of (Necklace 4):] by A17, ZFMISC_1:87;

then a in [: the carrier of (Necklace 4), the carrier of (Necklace 4):] \ the InternalRel of (Necklace 4) by A18, XBOOLE_0:def 5;

then A20: a in the InternalRel of (Necklace 4) ` by SUBSET_1:def 4;

not a in id the carrier of (Necklace 4) by A17, RELAT_1:def 10;

then a in ( the InternalRel of (Necklace 4) `) \ (id the carrier of (Necklace 4)) by A20, XBOOLE_0:def 5;

hence a in the InternalRel of (ComplRelStr (Necklace 4)) by NECKLACE:def 8; :: thesis: verum

end;proof

( 0 in the carrier of (Necklace 4) & 3 in the carrier of (Necklace 4) )
by A1, ENUMSET1:def 2;
assume A19:
a in the InternalRel of (Necklace 4)
; :: thesis: contradiction

end;per cases
( a = [0,1] or a = [1,0] or a = [1,2] or a = [2,1] or a = [2,3] or a = [3,2] )
by A19, ENUMSET1:def 4, NECKLA_2:2;

end;

then a in [: the carrier of (Necklace 4), the carrier of (Necklace 4):] by A17, ZFMISC_1:87;

then a in [: the carrier of (Necklace 4), the carrier of (Necklace 4):] \ the InternalRel of (Necklace 4) by A18, XBOOLE_0:def 5;

then A20: a in the InternalRel of (Necklace 4) ` by SUBSET_1:def 4;

not a in id the carrier of (Necklace 4) by A17, RELAT_1:def 10;

then a in ( the InternalRel of (Necklace 4) `) \ (id the carrier of (Necklace 4)) by A20, XBOOLE_0:def 5;

hence a in the InternalRel of (ComplRelStr (Necklace 4)) by NECKLACE:def 8; :: thesis: verum

suppose A21:
a = [3,0]
; :: thesis: a in the InternalRel of (ComplRelStr (Necklace 4))

A22:
not a in the InternalRel of (Necklace 4)

then a in [: the carrier of (Necklace 4), the carrier of (Necklace 4):] by A21, ZFMISC_1:87;

then a in [: the carrier of (Necklace 4), the carrier of (Necklace 4):] \ the InternalRel of (Necklace 4) by A22, XBOOLE_0:def 5;

then A24: a in the InternalRel of (Necklace 4) ` by SUBSET_1:def 4;

not a in id the carrier of (Necklace 4) by A21, RELAT_1:def 10;

then a in ( the InternalRel of (Necklace 4) `) \ (id the carrier of (Necklace 4)) by A24, XBOOLE_0:def 5;

hence a in the InternalRel of (ComplRelStr (Necklace 4)) by NECKLACE:def 8; :: thesis: verum

end;proof

( 0 in the carrier of (Necklace 4) & 3 in the carrier of (Necklace 4) )
by A1, ENUMSET1:def 2;
assume A23:
a in the InternalRel of (Necklace 4)
; :: thesis: contradiction

end;per cases
( a = [0,1] or a = [1,0] or a = [1,2] or a = [2,1] or a = [2,3] or a = [3,2] )
by A23, ENUMSET1:def 4, NECKLA_2:2;

end;

then a in [: the carrier of (Necklace 4), the carrier of (Necklace 4):] by A21, ZFMISC_1:87;

then a in [: the carrier of (Necklace 4), the carrier of (Necklace 4):] \ the InternalRel of (Necklace 4) by A22, XBOOLE_0:def 5;

then A24: a in the InternalRel of (Necklace 4) ` by SUBSET_1:def 4;

not a in id the carrier of (Necklace 4) by A21, RELAT_1:def 10;

then a in ( the InternalRel of (Necklace 4) `) \ (id the carrier of (Necklace 4)) by A24, XBOOLE_0:def 5;

hence a in the InternalRel of (ComplRelStr (Necklace 4)) by NECKLACE:def 8; :: thesis: verum

suppose A25:
a = [1,3]
; :: thesis: a in the InternalRel of (ComplRelStr (Necklace 4))

A26:
not a in the InternalRel of (Necklace 4)

then a in [: the carrier of (Necklace 4), the carrier of (Necklace 4):] by A25, ZFMISC_1:87;

then a in [: the carrier of (Necklace 4), the carrier of (Necklace 4):] \ the InternalRel of (Necklace 4) by A26, XBOOLE_0:def 5;

then A28: a in the InternalRel of (Necklace 4) ` by SUBSET_1:def 4;

not a in id the carrier of (Necklace 4) by A25, RELAT_1:def 10;

then a in ( the InternalRel of (Necklace 4) `) \ (id the carrier of (Necklace 4)) by A28, XBOOLE_0:def 5;

hence a in the InternalRel of (ComplRelStr (Necklace 4)) by NECKLACE:def 8; :: thesis: verum

end;proof

( 1 in the carrier of (Necklace 4) & 3 in the carrier of (Necklace 4) )
by A1, ENUMSET1:def 2;
assume A27:
a in the InternalRel of (Necklace 4)
; :: thesis: contradiction

end;per cases
( a = [0,1] or a = [1,0] or a = [1,2] or a = [2,1] or a = [2,3] or a = [3,2] )
by A27, ENUMSET1:def 4, NECKLA_2:2;

end;

then a in [: the carrier of (Necklace 4), the carrier of (Necklace 4):] by A25, ZFMISC_1:87;

then a in [: the carrier of (Necklace 4), the carrier of (Necklace 4):] \ the InternalRel of (Necklace 4) by A26, XBOOLE_0:def 5;

then A28: a in the InternalRel of (Necklace 4) ` by SUBSET_1:def 4;

not a in id the carrier of (Necklace 4) by A25, RELAT_1:def 10;

then a in ( the InternalRel of (Necklace 4) `) \ (id the carrier of (Necklace 4)) by A28, XBOOLE_0:def 5;

hence a in the InternalRel of (ComplRelStr (Necklace 4)) by NECKLACE:def 8; :: thesis: verum

suppose A29:
a = [3,1]
; :: thesis: a in the InternalRel of (ComplRelStr (Necklace 4))

A30:
not a in the InternalRel of (Necklace 4)

then a in [: the carrier of (Necklace 4), the carrier of (Necklace 4):] by A29, ZFMISC_1:87;

then a in [: the carrier of (Necklace 4), the carrier of (Necklace 4):] \ the InternalRel of (Necklace 4) by A30, XBOOLE_0:def 5;

then A32: a in the InternalRel of (Necklace 4) ` by SUBSET_1:def 4;

not a in id the carrier of (Necklace 4) by A29, RELAT_1:def 10;

then a in ( the InternalRel of (Necklace 4) `) \ (id the carrier of (Necklace 4)) by A32, XBOOLE_0:def 5;

hence a in the InternalRel of (ComplRelStr (Necklace 4)) by NECKLACE:def 8; :: thesis: verum

end;proof

( 1 in the carrier of (Necklace 4) & 3 in the carrier of (Necklace 4) )
by A1, ENUMSET1:def 2;
assume A31:
a in the InternalRel of (Necklace 4)
; :: thesis: contradiction

end;per cases
( a = [0,1] or a = [1,0] or a = [1,2] or a = [2,1] or a = [2,3] or a = [3,2] )
by A31, ENUMSET1:def 4, NECKLA_2:2;

end;

then a in [: the carrier of (Necklace 4), the carrier of (Necklace 4):] by A29, ZFMISC_1:87;

then a in [: the carrier of (Necklace 4), the carrier of (Necklace 4):] \ the InternalRel of (Necklace 4) by A30, XBOOLE_0:def 5;

then A32: a in the InternalRel of (Necklace 4) ` by SUBSET_1:def 4;

not a in id the carrier of (Necklace 4) by A29, RELAT_1:def 10;

then a in ( the InternalRel of (Necklace 4) `) \ (id the carrier of (Necklace 4)) by A32, XBOOLE_0:def 5;

hence a in the InternalRel of (ComplRelStr (Necklace 4)) by NECKLACE:def 8; :: thesis: verum