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:2, NECKLACE:21;
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 set ; :: 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 9;
then A3: ( x in the InternalRel of (Necklace 4) ` & not x in id the carrier of (Necklace 4) ) by XBOOLE_0:def 5;
then A4: ( x in [:the carrier of (Necklace 4),the carrier of (Necklace 4):] \ the InternalRel of (Necklace 4) & not x in id the carrier of (Necklace 4) ) by SUBSET_1:def 5;
consider a1, b1 being set such that
A5: ( a1 in the carrier of (Necklace 4) & b1 in the carrier of (Necklace 4) & 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, 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, 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 A5, 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 A5, 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 A5, 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 A5, 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 A5, 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 A5, 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, 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 A5, 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 A5, 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, 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 A5, 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 A5, 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, 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 A5, 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 A5, 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 set ; :: 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 A6: 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 A6, ENUMSET1:def 4;

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

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

proof

assume A9: 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 A9, ENUMSET1:def 4, NECKLA_2:2;

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

hence contradiction by A7, ZFMISC_1:33; :: thesis: verum

end;

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

hence contradiction by A7, ZFMISC_1:33; :: thesis: verum

end;

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

hence contradiction by A7, ZFMISC_1:33; :: thesis: verum

end;

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

hence contradiction by A7, ZFMISC_1:33; :: thesis: verum

end;

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

hence contradiction by A7, ZFMISC_1:33; :: thesis: verum

end;

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

hence contradiction by A7, ZFMISC_1:33; :: 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):] & not a in the InternalRel of (Necklace 4) & not a in id the carrier of (Necklace 4) ) by A7, A8, RELAT_1:def 10, ZFMISC_1:106;
then ( a in [:the carrier of (Necklace 4),the carrier of (Necklace 4):] \ the InternalRel of (Necklace 4) & not a in id the carrier of (Necklace 4) ) by XBOOLE_0:def 5;
then ( a in the InternalRel of (Necklace 4) ` & not a in id the carrier of (Necklace 4) ) by SUBSET_1:def 5;
then a in (the InternalRel of (Necklace 4) ` ) \ (id the carrier of (Necklace 4)) by XBOOLE_0:def 5;
hence a in the InternalRel of (ComplRelStr (Necklace 4)) by NECKLACE:def 9; :: thesis: verum

end;

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

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

proof

assume A12: 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 A12, ENUMSET1:def 4, NECKLA_2:2;

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

hence contradiction by A10, ZFMISC_1:33; :: thesis: verum

end;

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

hence contradiction by A10, ZFMISC_1:33; :: thesis: verum

end;

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

hence contradiction by A10, ZFMISC_1:33; :: thesis: verum

end;

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

hence contradiction by A10, ZFMISC_1:33; :: thesis: verum

end;

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

hence contradiction by A10, ZFMISC_1:33; :: thesis: verum

end;

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

hence contradiction by A10, ZFMISC_1:33; :: 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):] & not a in the InternalRel of (Necklace 4) & not a in id the carrier of (Necklace 4) ) by A10, A11, RELAT_1:def 10, ZFMISC_1:106;
then ( a in [:the carrier of (Necklace 4),the carrier of (Necklace 4):] \ the InternalRel of (Necklace 4) & not a in id the carrier of (Necklace 4) ) by XBOOLE_0:def 5;
then ( a in the InternalRel of (Necklace 4) ` & not a in id the carrier of (Necklace 4) ) by SUBSET_1:def 5;
then a in (the InternalRel of (Necklace 4) ` ) \ (id the carrier of (Necklace 4)) by XBOOLE_0:def 5;
hence a in the InternalRel of (ComplRelStr (Necklace 4)) by NECKLACE:def 9; :: thesis: verum

end;

suppose A13: a = [0 ,3] ; :: 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, ZFMISC_1:33; :: thesis: verum

end;

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

hence contradiction by A13, ZFMISC_1:33; :: thesis: verum

end;

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

hence contradiction by A13, ZFMISC_1:33; :: thesis: verum

end;

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

hence contradiction by A13, ZFMISC_1:33; :: thesis: verum

end;

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

hence contradiction by A13, ZFMISC_1:33; :: thesis: verum

end;

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

hence contradiction by A13, ZFMISC_1:33; :: 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):] & not a in the InternalRel of (Necklace 4) & not a in id the carrier of (Necklace 4) ) by A13, A14, RELAT_1:def 10, ZFMISC_1:106;
then ( a in [:the carrier of (Necklace 4),the carrier of (Necklace 4):] \ the InternalRel of (Necklace 4) & not a in id the carrier of (Necklace 4) ) by XBOOLE_0:def 5;
then ( a in the InternalRel of (Necklace 4) ` & not a in id the carrier of (Necklace 4) ) by SUBSET_1:def 5;
then a in (the InternalRel of (Necklace 4) ` ) \ (id the carrier of (Necklace 4)) by XBOOLE_0:def 5;
hence a in the InternalRel of (ComplRelStr (Necklace 4)) by NECKLACE:def 9; :: thesis: verum

end;

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

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

proof

assume A18: 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 A18, ENUMSET1:def 4, NECKLA_2:2;

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

hence contradiction by A16, ZFMISC_1:33; :: thesis: verum

end;

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

hence contradiction by A16, ZFMISC_1:33; :: thesis: verum

end;

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

hence contradiction by A16, ZFMISC_1:33; :: thesis: verum

end;

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

hence contradiction by A16, ZFMISC_1:33; :: thesis: verum

end;

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

hence contradiction by A16, ZFMISC_1:33; :: thesis: verum

end;

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

hence contradiction by A16, ZFMISC_1:33; :: 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):] & not a in the InternalRel of (Necklace 4) & not a in id the carrier of (Necklace 4) ) by A16, A17, RELAT_1:def 10, ZFMISC_1:106;
then ( a in [:the carrier of (Necklace 4),the carrier of (Necklace 4):] \ the InternalRel of (Necklace 4) & not a in id the carrier of (Necklace 4) ) by XBOOLE_0:def 5;
then ( a in the InternalRel of (Necklace 4) ` & not a in id the carrier of (Necklace 4) ) by SUBSET_1:def 5;
then a in (the InternalRel of (Necklace 4) ` ) \ (id the carrier of (Necklace 4)) by XBOOLE_0:def 5;
hence a in the InternalRel of (ComplRelStr (Necklace 4)) by NECKLACE:def 9; :: thesis: verum

end;

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

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

proof

assume A21: 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 A21, ENUMSET1:def 4, NECKLA_2:2;

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

hence contradiction by A19, ZFMISC_1:33; :: thesis: verum

end;

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

hence contradiction by A19, ZFMISC_1:33; :: thesis: verum

end;

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

hence contradiction by A19, ZFMISC_1:33; :: thesis: verum

end;

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

hence contradiction by A19, ZFMISC_1:33; :: thesis: verum

end;

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

hence contradiction by A19, ZFMISC_1:33; :: thesis: verum

end;

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

hence contradiction by A19, ZFMISC_1:33; :: 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):] & not a in the InternalRel of (Necklace 4) & not a in id the carrier of (Necklace 4) ) by A19, A20, RELAT_1:def 10, ZFMISC_1:106;
then ( a in [:the carrier of (Necklace 4),the carrier of (Necklace 4):] \ the InternalRel of (Necklace 4) & not a in id the carrier of (Necklace 4) ) by XBOOLE_0:def 5;
then ( a in the InternalRel of (Necklace 4) ` & not a in id the carrier of (Necklace 4) ) by SUBSET_1:def 5;
then a in (the InternalRel of (Necklace 4) ` ) \ (id the carrier of (Necklace 4)) by XBOOLE_0:def 5;
hence a in the InternalRel of (ComplRelStr (Necklace 4)) by NECKLACE:def 9; :: thesis: verum

end;

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

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

proof

assume A24: 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 A24, ENUMSET1:def 4, NECKLA_2:2;

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

hence contradiction by A22, ZFMISC_1:33; :: thesis: verum

end;

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

hence contradiction by A22, ZFMISC_1:33; :: thesis: verum

end;

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

hence contradiction by A22, ZFMISC_1:33; :: thesis: verum

end;

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

hence contradiction by A22, ZFMISC_1:33; :: thesis: verum

end;

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

hence contradiction by A22, ZFMISC_1:33; :: thesis: verum

end;

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

hence contradiction by A22, ZFMISC_1:33; :: 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):] & not a in the InternalRel of (Necklace 4) & not a in id the carrier of (Necklace 4) ) by A22, A23, RELAT_1:def 10, ZFMISC_1:106;
then ( a in [:the carrier of (Necklace 4),the carrier of (Necklace 4):] \ the InternalRel of (Necklace 4) & not a in id the carrier of (Necklace 4) ) by XBOOLE_0:def 5;
then ( a in the InternalRel of (Necklace 4) ` & not a in id the carrier of (Necklace 4) ) by SUBSET_1:def 5;
then a in (the InternalRel of (Necklace 4) ` ) \ (id the carrier of (Necklace 4)) by XBOOLE_0:def 5;
hence a in the InternalRel of (ComplRelStr (Necklace 4)) by NECKLACE:def 9; :: thesis: verum

end;

end;