set N4 = Necklace 4;
set cN4 = the carrier of ();
set CmpN4 = ComplRelStr ();
A1: the carrier of () = {0,1,2,3} by ;
thus the InternalRel of () 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 ()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the InternalRel of () or x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} )
assume x in the InternalRel of () ; :: thesis: x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]}
then A2: x in ( the InternalRel of () `) \ (id the carrier of ()) by NECKLACE:def 8;
then A3: not x in id the carrier of () by XBOOLE_0:def 5;
x in the InternalRel of () ` by ;
then A4: x in [: the carrier of (), the carrier of ():] \ the InternalRel of () by SUBSET_1:def 4;
consider a1, b1 being object such that
A5: a1 in the carrier of () and
A6: b1 in the carrier of () and
A7: x = [a1,b1] by ;
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 ;
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 ; :: 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 () by ;
hence x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} by ; :: 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 ; :: 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 ; :: 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 () by ;
hence x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} by ; :: 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 ; :: 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 ; :: 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 ; :: 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 () by ;
hence x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} by ; :: 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 ; :: 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 ; :: 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 () by ;
hence x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} by ; :: 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 () by ;
hence x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} by ; :: 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 ; :: 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 ; :: 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 () by ;
hence x in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} by ; :: 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 () )
assume A8: a in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]} ; :: thesis: a in the InternalRel of ()
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 ;
suppose A9: a = [0,2] ; :: thesis: a in the InternalRel of ()
A10: not a in the InternalRel of ()
proof
assume A11: a in the InternalRel of () ; :: thesis: contradiction
end;
( 0 in the carrier of () & 2 in the carrier of () ) by ;
then a in [: the carrier of (), the carrier of ():] by ;
then a in [: the carrier of (), the carrier of ():] \ the InternalRel of () by ;
then A12: a in the InternalRel of () ` by SUBSET_1:def 4;
not a in id the carrier of () by ;
then a in ( the InternalRel of () `) \ (id the carrier of ()) by ;
hence a in the InternalRel of () by NECKLACE:def 8; :: thesis: verum
end;
suppose A13: a = [2,0] ; :: thesis: a in the InternalRel of ()
A14: not a in the InternalRel of ()
proof
assume A15: a in the InternalRel of () ; :: thesis: contradiction
end;
( 0 in the carrier of () & 2 in the carrier of () ) by ;
then a in [: the carrier of (), the carrier of ():] by ;
then a in [: the carrier of (), the carrier of ():] \ the InternalRel of () by ;
then A16: a in the InternalRel of () ` by SUBSET_1:def 4;
not a in id the carrier of () by ;
then a in ( the InternalRel of () `) \ (id the carrier of ()) by ;
hence a in the InternalRel of () by NECKLACE:def 8; :: thesis: verum
end;
suppose A17: a = [0,3] ; :: thesis: a in the InternalRel of ()
A18: not a in the InternalRel of ()
proof
assume A19: a in the InternalRel of () ; :: thesis: contradiction
end;
( 0 in the carrier of () & 3 in the carrier of () ) by ;
then a in [: the carrier of (), the carrier of ():] by ;
then a in [: the carrier of (), the carrier of ():] \ the InternalRel of () by ;
then A20: a in the InternalRel of () ` by SUBSET_1:def 4;
not a in id the carrier of () by ;
then a in ( the InternalRel of () `) \ (id the carrier of ()) by ;
hence a in the InternalRel of () by NECKLACE:def 8; :: thesis: verum
end;
suppose A21: a = [3,0] ; :: thesis: a in the InternalRel of ()
A22: not a in the InternalRel of ()
proof
assume A23: a in the InternalRel of () ; :: thesis: contradiction
end;
( 0 in the carrier of () & 3 in the carrier of () ) by ;
then a in [: the carrier of (), the carrier of ():] by ;
then a in [: the carrier of (), the carrier of ():] \ the InternalRel of () by ;
then A24: a in the InternalRel of () ` by SUBSET_1:def 4;
not a in id the carrier of () by ;
then a in ( the InternalRel of () `) \ (id the carrier of ()) by ;
hence a in the InternalRel of () by NECKLACE:def 8; :: thesis: verum
end;
suppose A25: a = [1,3] ; :: thesis: a in the InternalRel of ()
A26: not a in the InternalRel of ()
proof
assume A27: a in the InternalRel of () ; :: thesis: contradiction
end;
( 1 in the carrier of () & 3 in the carrier of () ) by ;
then a in [: the carrier of (), the carrier of ():] by ;
then a in [: the carrier of (), the carrier of ():] \ the InternalRel of () by ;
then A28: a in the InternalRel of () ` by SUBSET_1:def 4;
not a in id the carrier of () by ;
then a in ( the InternalRel of () `) \ (id the carrier of ()) by ;
hence a in the InternalRel of () by NECKLACE:def 8; :: thesis: verum
end;
suppose A29: a = [3,1] ; :: thesis: a in the InternalRel of ()
A30: not a in the InternalRel of ()
proof
assume A31: a in the InternalRel of () ; :: thesis: contradiction
end;
( 1 in the carrier of () & 3 in the carrier of () ) by ;
then a in [: the carrier of (), the carrier of ():] by ;
then a in [: the carrier of (), the carrier of ():] \ the InternalRel of () by ;
then A32: a in the InternalRel of () ` by SUBSET_1:def 4;
not a in id the carrier of () by ;
then a in ( the InternalRel of () `) \ (id the carrier of ()) by ;
hence a in the InternalRel of () by NECKLACE:def 8; :: thesis: verum
end;
end;