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))

proof

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;

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;

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

hence x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} by A3, A5, A7, RELAT_1:def 10; :: thesis: verum

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;

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

hence x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} by A7, ENUMSET1:def 4; :: thesis: verum

end;

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

hence x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} by A7, ENUMSET1:def 4; :: thesis: verum

end;

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;

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

hence x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} by A7, ENUMSET1:def 4; :: thesis: verum

end;

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

hence x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} by A7, ENUMSET1:def 4; :: thesis: verum

end;

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

hence x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} by A3, A5, A7, RELAT_1:def 10; :: thesis: verum

end;

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;

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

hence x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} by A7, ENUMSET1:def 4; :: thesis: verum

end;

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

hence x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} by A3, A5, A7, RELAT_1:def 10; :: thesis: verum

end;

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;

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;

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

hence x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} by A3, A5, A7, RELAT_1:def 10; :: thesis: verum

end;

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

hence x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} by A7, ENUMSET1:def 4; :: thesis: verum

end;

suppose ( a1 = 3 & 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;

end;

end;

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)) )
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;

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

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

proof

assume A11: a in the InternalRel of (Necklace 4) ; :: thesis: contradiction

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;

suppose a = [0,1] ; :: thesis: contradiction

hence contradiction by A9, XTUPLE_0:1; :: thesis: verum

end;

suppose a = [1,0] ; :: thesis: contradiction

hence contradiction by A9, XTUPLE_0:1; :: thesis: verum

end;

suppose a = [1,2] ; :: thesis: contradiction

hence contradiction by A9, XTUPLE_0:1; :: thesis: verum

end;

suppose a = [2,1] ; :: thesis: contradiction

hence contradiction by A9, XTUPLE_0:1; :: thesis: verum

end;

suppose a = [2,3] ; :: thesis: contradiction

hence contradiction by A9, XTUPLE_0:1; :: thesis: verum

end;

suppose a = [3,2] ; :: thesis: contradiction

hence contradiction by A9, XTUPLE_0:1; :: thesis: verum

end;

end;

end;

( 0 in the carrier of (Necklace 4) & 2 in the carrier of (Necklace 4) ) by A1, ENUMSET1:def 2;
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;

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

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

proof

assume A15: a in the InternalRel of (Necklace 4) ; :: thesis: contradiction

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;

suppose a = [0,1] ; :: thesis: contradiction

hence contradiction by A13, XTUPLE_0:1; :: thesis: verum

end;

suppose a = [1,0] ; :: thesis: contradiction

hence contradiction by A13, XTUPLE_0:1; :: thesis: verum

end;

suppose a = [1,2] ; :: thesis: contradiction

hence contradiction by A13, XTUPLE_0:1; :: thesis: verum

end;

suppose a = [2,1] ; :: thesis: contradiction

hence contradiction by A13, XTUPLE_0:1; :: thesis: verum

end;

suppose a = [2,3] ; :: thesis: contradiction

hence contradiction by A13, XTUPLE_0:1; :: thesis: verum

end;

suppose a = [3,2] ; :: thesis: contradiction

hence contradiction by A13, XTUPLE_0:1; :: thesis: verum

end;

end;

end;

( 0 in the carrier of (Necklace 4) & 2 in the carrier of (Necklace 4) ) by A1, ENUMSET1:def 2;
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;

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

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

proof

assume A19: a in the InternalRel of (Necklace 4) ; :: thesis: contradiction

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;

suppose a = [0,1] ; :: thesis: contradiction

hence contradiction by A17, XTUPLE_0:1; :: thesis: verum

end;

suppose a = [1,0] ; :: thesis: contradiction

hence contradiction by A17, XTUPLE_0:1; :: thesis: verum

end;

suppose a = [1,2] ; :: thesis: contradiction

hence contradiction by A17, XTUPLE_0:1; :: thesis: verum

end;

suppose a = [2,1] ; :: thesis: contradiction

hence contradiction by A17, XTUPLE_0:1; :: thesis: verum

end;

suppose a = [2,3] ; :: thesis: contradiction

hence contradiction by A17, XTUPLE_0:1; :: thesis: verum

end;

suppose a = [3,2] ; :: thesis: contradiction

hence contradiction by A17, XTUPLE_0:1; :: thesis: verum

end;

end;

end;

( 0 in the carrier of (Necklace 4) & 3 in the carrier of (Necklace 4) ) by A1, ENUMSET1:def 2;
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;

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

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

proof

assume A23: a in the InternalRel of (Necklace 4) ; :: thesis: contradiction

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;

suppose a = [0,1] ; :: thesis: contradiction

hence contradiction by A21, XTUPLE_0:1; :: thesis: verum

end;

suppose a = [1,0] ; :: thesis: contradiction

hence contradiction by A21, XTUPLE_0:1; :: thesis: verum

end;

suppose a = [1,2] ; :: thesis: contradiction

hence contradiction by A21, XTUPLE_0:1; :: thesis: verum

end;

suppose a = [2,1] ; :: thesis: contradiction

hence contradiction by A21, XTUPLE_0:1; :: thesis: verum

end;

suppose a = [2,3] ; :: thesis: contradiction

hence contradiction by A21, XTUPLE_0:1; :: thesis: verum

end;

suppose a = [3,2] ; :: thesis: contradiction

hence contradiction by A21, XTUPLE_0:1; :: thesis: verum

end;

end;

end;

( 0 in the carrier of (Necklace 4) & 3 in the carrier of (Necklace 4) ) by A1, ENUMSET1:def 2;
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;

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

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

proof

assume A27: a in the InternalRel of (Necklace 4) ; :: thesis: contradiction

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;

suppose a = [0,1] ; :: thesis: contradiction

hence contradiction by A25, XTUPLE_0:1; :: thesis: verum

end;

suppose a = [1,0] ; :: thesis: contradiction

hence contradiction by A25, XTUPLE_0:1; :: thesis: verum

end;

suppose a = [1,2] ; :: thesis: contradiction

hence contradiction by A25, XTUPLE_0:1; :: thesis: verum

end;

suppose a = [2,1] ; :: thesis: contradiction

hence contradiction by A25, XTUPLE_0:1; :: thesis: verum

end;

suppose a = [2,3] ; :: thesis: contradiction

hence contradiction by A25, XTUPLE_0:1; :: thesis: verum

end;

suppose a = [3,2] ; :: thesis: contradiction

hence contradiction by A25, XTUPLE_0:1; :: thesis: verum

end;

end;

end;

( 1 in the carrier of (Necklace 4) & 3 in the carrier of (Necklace 4) ) by A1, ENUMSET1:def 2;
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;

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

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

proof

assume A31: a in the InternalRel of (Necklace 4) ; :: thesis: contradiction

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;

suppose a = [0,1] ; :: thesis: contradiction

hence contradiction by A29, XTUPLE_0:1; :: thesis: verum

end;

suppose a = [1,0] ; :: thesis: contradiction

hence contradiction by A29, XTUPLE_0:1; :: thesis: verum

end;

suppose a = [1,2] ; :: thesis: contradiction

hence contradiction by A29, XTUPLE_0:1; :: thesis: verum

end;

suppose a = [2,1] ; :: thesis: contradiction

hence contradiction by A29, XTUPLE_0:1; :: thesis: verum

end;

suppose a = [2,3] ; :: thesis: contradiction

hence contradiction by A29, XTUPLE_0:1; :: thesis: verum

end;

suppose a = [3,2] ; :: thesis: contradiction

hence contradiction by A29, XTUPLE_0:1; :: thesis: verum

end;

end;

end;

( 1 in the carrier of (Necklace 4) & 3 in the carrier of (Necklace 4) ) by A1, ENUMSET1:def 2;
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;

end;