let G be non empty irreflexive RelStr ; :: thesis: ( G embeds Necklace 4 iff ComplRelStr G embeds Necklace 4 )

set N4 = Necklace 4;

set CmpN4 = ComplRelStr (Necklace 4);

set CmpG = ComplRelStr G;

A1: the carrier of (ComplRelStr G) = the carrier of G by NECKLACE:def 8;

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

then A3: 0 in the carrier of (Necklace 4) by ENUMSET1:def 2;

A4: the carrier of (ComplRelStr (Necklace 4)) = the carrier of (Necklace 4) by NECKLACE:def 8;

thus ( G embeds Necklace 4 implies ComplRelStr G embeds Necklace 4 ) :: thesis: ( ComplRelStr G embeds Necklace 4 implies G embeds Necklace 4 )

then consider f being Function of (Necklace 4),(ComplRelStr G) such that

A57: f is V24() and

A58: for x, y being Element of (Necklace 4) holds

( [x,y] in the InternalRel of (Necklace 4) iff [(f . x),(f . y)] in the InternalRel of (ComplRelStr G) ) ;

consider g being Function of (Necklace 4),(ComplRelStr (Necklace 4)) such that

A59: g is isomorphic by NECKLACE:29, WAYBEL_1:def 8;

A60: 2 in the carrier of (Necklace 4) by A2, ENUMSET1:def 2;

A61: dom f = the carrier of (Necklace 4) by FUNCT_2:def 1;

A62: [(f . 0),(f . 2)] in the InternalRel of G

A67: [(f . 0),(f . 3)] in the InternalRel of G

A72: [(f . 1),(f . 3)] in the InternalRel of G

then A76: [(f . 3),(f . 2)] in the InternalRel of (ComplRelStr G) by A58, A60, A66;

[2,3] in the InternalRel of (Necklace 4) by ENUMSET1:def 4, NECKLA_2:2;

then A77: [(f . 2),(f . 3)] in the InternalRel of (ComplRelStr G) by A58, A60, A66;

[1,2] in the InternalRel of (Necklace 4) by ENUMSET1:def 4, NECKLA_2:2;

then A78: [(f . 1),(f . 2)] in the InternalRel of (ComplRelStr G) by A58, A71, A60;

[1,0] in the InternalRel of (Necklace 4) by ENUMSET1:def 4, NECKLA_2:2;

then A79: [(f . 1),(f . 0)] in the InternalRel of (ComplRelStr G) by A58, A3, A71;

A80: [(f . 2),(f . 0)] in the InternalRel of G

then A92: [(f . 2),(f . 1)] in the InternalRel of (ComplRelStr G) by A58, A71, A60;

[0,1] in the InternalRel of (Necklace 4) by ENUMSET1:def 4, NECKLA_2:2;

then A93: [(f . 0),(f . 1)] in the InternalRel of (ComplRelStr G) by A58, A3, A71;

A94: for x, y being Element of (ComplRelStr (Necklace 4)) holds

( [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) iff [(f . x),(f . y)] in the InternalRel of G )

reconsider h = f * g as Function of (Necklace 4),G ;

A108: ( g is V24() & g is monotone ) by A59, WAYBEL_0:def 38;

for x, y being Element of (Necklace 4) holds

( [x,y] in the InternalRel of (Necklace 4) iff [(h . x),(h . y)] in the InternalRel of G )

set N4 = Necklace 4;

set CmpN4 = ComplRelStr (Necklace 4);

set CmpG = ComplRelStr G;

A1: the carrier of (ComplRelStr G) = the carrier of G by NECKLACE:def 8;

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

then A3: 0 in the carrier of (Necklace 4) by ENUMSET1:def 2;

A4: the carrier of (ComplRelStr (Necklace 4)) = the carrier of (Necklace 4) by NECKLACE:def 8;

thus ( G embeds Necklace 4 implies ComplRelStr G embeds Necklace 4 ) :: thesis: ( ComplRelStr G embeds Necklace 4 implies G embeds Necklace 4 )

proof

assume
ComplRelStr G embeds Necklace 4
; :: thesis: G embeds Necklace 4
ComplRelStr (Necklace 4), Necklace 4 are_isomorphic
by NECKLACE:29, WAYBEL_1:6;

then consider g being Function of (ComplRelStr (Necklace 4)),(Necklace 4) such that

A5: g is isomorphic by WAYBEL_1:def 8;

assume G embeds Necklace 4 ; :: thesis: ComplRelStr G embeds Necklace 4

then consider f being Function of (Necklace 4),G such that

A6: f is V24() and

A7: for x, y being Element of (Necklace 4) holds

( [x,y] in the InternalRel of (Necklace 4) iff [(f . x),(f . y)] in the InternalRel of G ) ;

reconsider h = f * g as Function of (ComplRelStr (Necklace 4)),G ;

A8: ( g is V24() & g is monotone ) by A5, WAYBEL_0:def 38;

A9: for x, y being Element of (ComplRelStr (Necklace 4)) holds

( [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) iff [(h . x),(h . y)] in the InternalRel of G )

A11: 1 in the carrier of (ComplRelStr (Necklace 4)) by A2, A4, ENUMSET1:def 2;

A12: dom h = the carrier of (ComplRelStr (Necklace 4)) by FUNCT_2:def 1;

A13: [(h . 0),(h . 1)] in the InternalRel of (ComplRelStr G)

A18: [(h . 1),(h . 2)] in the InternalRel of (ComplRelStr G)

A23: [(h . 2),(h . 3)] in the InternalRel of (ComplRelStr G)

then A27: [(h . 3),(h . 1)] in the InternalRel of G by A9, A11, A22;

[1,3] in the InternalRel of (ComplRelStr (Necklace 4)) by Th11, ENUMSET1:def 4;

then A28: [(h . 1),(h . 3)] in the InternalRel of G by A9, A11, A22;

[3,0] in the InternalRel of (ComplRelStr (Necklace 4)) by Th11, ENUMSET1:def 4;

then A29: [(h . 3),(h . 0)] in the InternalRel of G by A9, A10, A22;

[0,3] in the InternalRel of (ComplRelStr (Necklace 4)) by Th11, ENUMSET1:def 4;

then A30: [(h . 0),(h . 3)] in the InternalRel of G by A9, A10, A22;

A31: [(h . 1),(h . 0)] in the InternalRel of (ComplRelStr G)

then A43: [(h . 2),(h . 0)] in the InternalRel of G by A9, A10, A17;

[0,2] in the InternalRel of (ComplRelStr (Necklace 4)) by Th11, ENUMSET1:def 4;

then A44: [(h . 0),(h . 2)] in the InternalRel of G by A9, A10, A17;

for x, y being Element of (Necklace 4) holds

( [x,y] in the InternalRel of (Necklace 4) iff [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) )

end;then consider g being Function of (ComplRelStr (Necklace 4)),(Necklace 4) such that

A5: g is isomorphic by WAYBEL_1:def 8;

assume G embeds Necklace 4 ; :: thesis: ComplRelStr G embeds Necklace 4

then consider f being Function of (Necklace 4),G such that

A6: f is V24() and

A7: for x, y being Element of (Necklace 4) holds

( [x,y] in the InternalRel of (Necklace 4) iff [(f . x),(f . y)] in the InternalRel of G ) ;

reconsider h = f * g as Function of (ComplRelStr (Necklace 4)),G ;

A8: ( g is V24() & g is monotone ) by A5, WAYBEL_0:def 38;

A9: for x, y being Element of (ComplRelStr (Necklace 4)) holds

( [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) iff [(h . x),(h . y)] in the InternalRel of G )

proof

A10:
0 in the carrier of (ComplRelStr (Necklace 4))
by A2, A4, ENUMSET1:def 2;
let x, y be Element of (ComplRelStr (Necklace 4)); :: thesis: ( [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) iff [(h . x),(h . y)] in the InternalRel of G )

thus ( [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) implies [(h . x),(h . y)] in the InternalRel of G ) :: thesis: ( [(h . x),(h . y)] in the InternalRel of G implies [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) )

then [(f . (g . x)),(h . y)] in the InternalRel of G by FUNCT_2:15;

then [(f . (g . x)),(f . (g . y))] in the InternalRel of G by FUNCT_2:15;

then [(g . x),(g . y)] in the InternalRel of (Necklace 4) by A7;

then g . x <= g . y by ORDERS_2:def 5;

then x <= y by A5, WAYBEL_0:66;

hence [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) by ORDERS_2:def 5; :: thesis: verum

end;thus ( [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) implies [(h . x),(h . y)] in the InternalRel of G ) :: thesis: ( [(h . x),(h . y)] in the InternalRel of G implies [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) )

proof

assume
[(h . x),(h . y)] in the InternalRel of G
; :: thesis: [x,y] in the InternalRel of (ComplRelStr (Necklace 4))
assume
[x,y] in the InternalRel of (ComplRelStr (Necklace 4))
; :: thesis: [(h . x),(h . y)] in the InternalRel of G

then x <= y by ORDERS_2:def 5;

then g . x <= g . y by A8, WAYBEL_1:def 2;

then [(g . x),(g . y)] in the InternalRel of (Necklace 4) by ORDERS_2:def 5;

then [(f . (g . x)),(f . (g . y))] in the InternalRel of G by A7;

then [((f * g) . x),(f . (g . y))] in the InternalRel of G by FUNCT_2:15;

hence [(h . x),(h . y)] in the InternalRel of G by FUNCT_2:15; :: thesis: verum

end;then x <= y by ORDERS_2:def 5;

then g . x <= g . y by A8, WAYBEL_1:def 2;

then [(g . x),(g . y)] in the InternalRel of (Necklace 4) by ORDERS_2:def 5;

then [(f . (g . x)),(f . (g . y))] in the InternalRel of G by A7;

then [((f * g) . x),(f . (g . y))] in the InternalRel of G by FUNCT_2:15;

hence [(h . x),(h . y)] in the InternalRel of G by FUNCT_2:15; :: thesis: verum

then [(f . (g . x)),(h . y)] in the InternalRel of G by FUNCT_2:15;

then [(f . (g . x)),(f . (g . y))] in the InternalRel of G by FUNCT_2:15;

then [(g . x),(g . y)] in the InternalRel of (Necklace 4) by A7;

then g . x <= g . y by ORDERS_2:def 5;

then x <= y by A5, WAYBEL_0:66;

hence [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) by ORDERS_2:def 5; :: thesis: verum

A11: 1 in the carrier of (ComplRelStr (Necklace 4)) by A2, A4, ENUMSET1:def 2;

A12: dom h = the carrier of (ComplRelStr (Necklace 4)) by FUNCT_2:def 1;

A13: [(h . 0),(h . 1)] in the InternalRel of (ComplRelStr G)

proof

A17:
2 in the carrier of (ComplRelStr (Necklace 4))
by A2, A4, ENUMSET1:def 2;
assume A14:
not [(h . 0),(h . 1)] in the InternalRel of (ComplRelStr G)
; :: thesis: contradiction

[(h . 0),(h . 1)] in the InternalRel of G

[0,1] in the InternalRel of (Necklace 4) by ENUMSET1:def 4, NECKLA_2:2;

then [0,1] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A16, XBOOLE_0:def 4;

then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;

hence contradiction by Th12; :: thesis: verum

end;[(h . 0),(h . 1)] in the InternalRel of G

proof

then A16:
[0,1] in the InternalRel of (ComplRelStr (Necklace 4))
by A9, A10, A11;
( h . 0 in the carrier of G & h . 1 in the carrier of G )
by A10, A11, FUNCT_2:5;

then [(h . 0),(h . 1)] in [: the carrier of G, the carrier of G:] by ZFMISC_1:87;

then [(h . 0),(h . 1)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;

then A15: ( [(h . 0),(h . 1)] in (id the carrier of G) \/ the InternalRel of G or [(h . 0),(h . 1)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;

assume not [(h . 0),(h . 1)] in the InternalRel of G ; :: thesis: contradiction

then [(h . 0),(h . 1)] in id the carrier of G by A14, A15, XBOOLE_0:def 3;

then h . 0 = h . 1 by RELAT_1:def 10;

hence contradiction by A6, A8, A12, A10, A11, FUNCT_1:def 4; :: thesis: verum

end;then [(h . 0),(h . 1)] in [: the carrier of G, the carrier of G:] by ZFMISC_1:87;

then [(h . 0),(h . 1)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;

then A15: ( [(h . 0),(h . 1)] in (id the carrier of G) \/ the InternalRel of G or [(h . 0),(h . 1)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;

assume not [(h . 0),(h . 1)] in the InternalRel of G ; :: thesis: contradiction

then [(h . 0),(h . 1)] in id the carrier of G by A14, A15, XBOOLE_0:def 3;

then h . 0 = h . 1 by RELAT_1:def 10;

hence contradiction by A6, A8, A12, A10, A11, FUNCT_1:def 4; :: thesis: verum

[0,1] in the InternalRel of (Necklace 4) by ENUMSET1:def 4, NECKLA_2:2;

then [0,1] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A16, XBOOLE_0:def 4;

then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;

hence contradiction by Th12; :: thesis: verum

A18: [(h . 1),(h . 2)] in the InternalRel of (ComplRelStr G)

proof

A22:
3 in the carrier of (ComplRelStr (Necklace 4))
by A2, A4, ENUMSET1:def 2;
assume A19:
not [(h . 1),(h . 2)] in the InternalRel of (ComplRelStr G)
; :: thesis: contradiction

[(h . 1),(h . 2)] in the InternalRel of G

[1,2] in the InternalRel of (Necklace 4) by ENUMSET1:def 4, NECKLA_2:2;

then [1,2] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A21, XBOOLE_0:def 4;

then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;

hence contradiction by Th12; :: thesis: verum

end;[(h . 1),(h . 2)] in the InternalRel of G

proof

then A21:
[1,2] in the InternalRel of (ComplRelStr (Necklace 4))
by A9, A11, A17;
( h . 1 in the carrier of G & h . 2 in the carrier of G )
by A11, A17, FUNCT_2:5;

then [(h . 1),(h . 2)] in [: the carrier of G, the carrier of G:] by ZFMISC_1:87;

then [(h . 1),(h . 2)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;

then A20: ( [(h . 1),(h . 2)] in (id the carrier of G) \/ the InternalRel of G or [(h . 1),(h . 2)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;

assume not [(h . 1),(h . 2)] in the InternalRel of G ; :: thesis: contradiction

then [(h . 1),(h . 2)] in id the carrier of G by A19, A20, XBOOLE_0:def 3;

then h . 1 = h . 2 by RELAT_1:def 10;

hence contradiction by A6, A8, A12, A11, A17, FUNCT_1:def 4; :: thesis: verum

end;then [(h . 1),(h . 2)] in [: the carrier of G, the carrier of G:] by ZFMISC_1:87;

then [(h . 1),(h . 2)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;

then A20: ( [(h . 1),(h . 2)] in (id the carrier of G) \/ the InternalRel of G or [(h . 1),(h . 2)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;

assume not [(h . 1),(h . 2)] in the InternalRel of G ; :: thesis: contradiction

then [(h . 1),(h . 2)] in id the carrier of G by A19, A20, XBOOLE_0:def 3;

then h . 1 = h . 2 by RELAT_1:def 10;

hence contradiction by A6, A8, A12, A11, A17, FUNCT_1:def 4; :: thesis: verum

[1,2] in the InternalRel of (Necklace 4) by ENUMSET1:def 4, NECKLA_2:2;

then [1,2] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A21, XBOOLE_0:def 4;

then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;

hence contradiction by Th12; :: thesis: verum

A23: [(h . 2),(h . 3)] in the InternalRel of (ComplRelStr G)

proof

[3,1] in the InternalRel of (ComplRelStr (Necklace 4))
by Th11, ENUMSET1:def 4;
assume A24:
not [(h . 2),(h . 3)] in the InternalRel of (ComplRelStr G)
; :: thesis: contradiction

[(h . 2),(h . 3)] in the InternalRel of G

[2,3] in the InternalRel of (Necklace 4) by ENUMSET1:def 4, NECKLA_2:2;

then [2,3] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A26, XBOOLE_0:def 4;

then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;

hence contradiction by Th12; :: thesis: verum

end;[(h . 2),(h . 3)] in the InternalRel of G

proof

then A26:
[2,3] in the InternalRel of (ComplRelStr (Necklace 4))
by A9, A17, A22;
( h . 2 in the carrier of G & h . 3 in the carrier of G )
by A17, A22, FUNCT_2:5;

then [(h . 2),(h . 3)] in [: the carrier of G, the carrier of G:] by ZFMISC_1:87;

then [(h . 2),(h . 3)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;

then A25: ( [(h . 2),(h . 3)] in (id the carrier of G) \/ the InternalRel of G or [(h . 2),(h . 3)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;

assume not [(h . 2),(h . 3)] in the InternalRel of G ; :: thesis: contradiction

then [(h . 2),(h . 3)] in id the carrier of G by A24, A25, XBOOLE_0:def 3;

then h . 2 = h . 3 by RELAT_1:def 10;

hence contradiction by A6, A8, A12, A17, A22, FUNCT_1:def 4; :: thesis: verum

end;then [(h . 2),(h . 3)] in [: the carrier of G, the carrier of G:] by ZFMISC_1:87;

then [(h . 2),(h . 3)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;

then A25: ( [(h . 2),(h . 3)] in (id the carrier of G) \/ the InternalRel of G or [(h . 2),(h . 3)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;

assume not [(h . 2),(h . 3)] in the InternalRel of G ; :: thesis: contradiction

then [(h . 2),(h . 3)] in id the carrier of G by A24, A25, XBOOLE_0:def 3;

then h . 2 = h . 3 by RELAT_1:def 10;

hence contradiction by A6, A8, A12, A17, A22, FUNCT_1:def 4; :: thesis: verum

[2,3] in the InternalRel of (Necklace 4) by ENUMSET1:def 4, NECKLA_2:2;

then [2,3] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A26, XBOOLE_0:def 4;

then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;

hence contradiction by Th12; :: thesis: verum

then A27: [(h . 3),(h . 1)] in the InternalRel of G by A9, A11, A22;

[1,3] in the InternalRel of (ComplRelStr (Necklace 4)) by Th11, ENUMSET1:def 4;

then A28: [(h . 1),(h . 3)] in the InternalRel of G by A9, A11, A22;

[3,0] in the InternalRel of (ComplRelStr (Necklace 4)) by Th11, ENUMSET1:def 4;

then A29: [(h . 3),(h . 0)] in the InternalRel of G by A9, A10, A22;

[0,3] in the InternalRel of (ComplRelStr (Necklace 4)) by Th11, ENUMSET1:def 4;

then A30: [(h . 0),(h . 3)] in the InternalRel of G by A9, A10, A22;

A31: [(h . 1),(h . 0)] in the InternalRel of (ComplRelStr G)

proof

A35:
[(h . 2),(h . 1)] in the InternalRel of (ComplRelStr G)
assume A32:
not [(h . 1),(h . 0)] in the InternalRel of (ComplRelStr G)
; :: thesis: contradiction

[(h . 1),(h . 0)] in the InternalRel of G

[1,0] in the InternalRel of (Necklace 4) by ENUMSET1:def 4, NECKLA_2:2;

then [1,0] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A34, XBOOLE_0:def 4;

then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;

hence contradiction by Th12; :: thesis: verum

end;[(h . 1),(h . 0)] in the InternalRel of G

proof

then A34:
[1,0] in the InternalRel of (ComplRelStr (Necklace 4))
by A9, A10, A11;
( h . 0 in the carrier of G & h . 1 in the carrier of G )
by A10, A11, FUNCT_2:5;

then [(h . 1),(h . 0)] in [: the carrier of G, the carrier of G:] by ZFMISC_1:87;

then [(h . 1),(h . 0)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;

then A33: ( [(h . 1),(h . 0)] in (id the carrier of G) \/ the InternalRel of G or [(h . 1),(h . 0)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;

assume not [(h . 1),(h . 0)] in the InternalRel of G ; :: thesis: contradiction

then [(h . 1),(h . 0)] in id the carrier of G by A32, A33, XBOOLE_0:def 3;

then h . 0 = h . 1 by RELAT_1:def 10;

hence contradiction by A6, A8, A12, A10, A11, FUNCT_1:def 4; :: thesis: verum

end;then [(h . 1),(h . 0)] in [: the carrier of G, the carrier of G:] by ZFMISC_1:87;

then [(h . 1),(h . 0)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;

then A33: ( [(h . 1),(h . 0)] in (id the carrier of G) \/ the InternalRel of G or [(h . 1),(h . 0)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;

assume not [(h . 1),(h . 0)] in the InternalRel of G ; :: thesis: contradiction

then [(h . 1),(h . 0)] in id the carrier of G by A32, A33, XBOOLE_0:def 3;

then h . 0 = h . 1 by RELAT_1:def 10;

hence contradiction by A6, A8, A12, A10, A11, FUNCT_1:def 4; :: thesis: verum

[1,0] in the InternalRel of (Necklace 4) by ENUMSET1:def 4, NECKLA_2:2;

then [1,0] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A34, XBOOLE_0:def 4;

then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;

hence contradiction by Th12; :: thesis: verum

proof

A39:
[(h . 3),(h . 2)] in the InternalRel of (ComplRelStr G)
assume A36:
not [(h . 2),(h . 1)] in the InternalRel of (ComplRelStr G)
; :: thesis: contradiction

[(h . 2),(h . 1)] in the InternalRel of G

[2,1] in the InternalRel of (Necklace 4) by ENUMSET1:def 4, NECKLA_2:2;

then [2,1] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A38, XBOOLE_0:def 4;

then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;

hence contradiction by Th12; :: thesis: verum

end;[(h . 2),(h . 1)] in the InternalRel of G

proof

then A38:
[2,1] in the InternalRel of (ComplRelStr (Necklace 4))
by A9, A11, A17;
( h . 1 in the carrier of G & h . 2 in the carrier of G )
by A11, A17, FUNCT_2:5;

then [(h . 2),(h . 1)] in [: the carrier of G, the carrier of G:] by ZFMISC_1:87;

then [(h . 2),(h . 1)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;

then A37: ( [(h . 2),(h . 1)] in (id the carrier of G) \/ the InternalRel of G or [(h . 2),(h . 1)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;

assume not [(h . 2),(h . 1)] in the InternalRel of G ; :: thesis: contradiction

then [(h . 2),(h . 1)] in id the carrier of G by A36, A37, XBOOLE_0:def 3;

then h . 1 = h . 2 by RELAT_1:def 10;

hence contradiction by A6, A8, A12, A11, A17, FUNCT_1:def 4; :: thesis: verum

end;then [(h . 2),(h . 1)] in [: the carrier of G, the carrier of G:] by ZFMISC_1:87;

then [(h . 2),(h . 1)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;

then A37: ( [(h . 2),(h . 1)] in (id the carrier of G) \/ the InternalRel of G or [(h . 2),(h . 1)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;

assume not [(h . 2),(h . 1)] in the InternalRel of G ; :: thesis: contradiction

then [(h . 2),(h . 1)] in id the carrier of G by A36, A37, XBOOLE_0:def 3;

then h . 1 = h . 2 by RELAT_1:def 10;

hence contradiction by A6, A8, A12, A11, A17, FUNCT_1:def 4; :: thesis: verum

[2,1] in the InternalRel of (Necklace 4) by ENUMSET1:def 4, NECKLA_2:2;

then [2,1] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A38, XBOOLE_0:def 4;

then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;

hence contradiction by Th12; :: thesis: verum

proof

[2,0] in the InternalRel of (ComplRelStr (Necklace 4))
by Th11, ENUMSET1:def 4;
assume A40:
not [(h . 3),(h . 2)] in the InternalRel of (ComplRelStr G)
; :: thesis: contradiction

[(h . 3),(h . 2)] in the InternalRel of G

[3,2] in the InternalRel of (Necklace 4) by ENUMSET1:def 4, NECKLA_2:2;

then [3,2] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A42, XBOOLE_0:def 4;

then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;

hence contradiction by Th12; :: thesis: verum

end;[(h . 3),(h . 2)] in the InternalRel of G

proof

then A42:
[3,2] in the InternalRel of (ComplRelStr (Necklace 4))
by A9, A17, A22;
( h . 2 in the carrier of G & h . 3 in the carrier of G )
by A17, A22, FUNCT_2:5;

then [(h . 3),(h . 2)] in [: the carrier of G, the carrier of G:] by ZFMISC_1:87;

then [(h . 3),(h . 2)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;

then A41: ( [(h . 3),(h . 2)] in (id the carrier of G) \/ the InternalRel of G or [(h . 3),(h . 2)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;

assume not [(h . 3),(h . 2)] in the InternalRel of G ; :: thesis: contradiction

then [(h . 3),(h . 2)] in id the carrier of G by A40, A41, XBOOLE_0:def 3;

then h . 2 = h . 3 by RELAT_1:def 10;

hence contradiction by A6, A8, A12, A17, A22, FUNCT_1:def 4; :: thesis: verum

end;then [(h . 3),(h . 2)] in [: the carrier of G, the carrier of G:] by ZFMISC_1:87;

then [(h . 3),(h . 2)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;

then A41: ( [(h . 3),(h . 2)] in (id the carrier of G) \/ the InternalRel of G or [(h . 3),(h . 2)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;

assume not [(h . 3),(h . 2)] in the InternalRel of G ; :: thesis: contradiction

then [(h . 3),(h . 2)] in id the carrier of G by A40, A41, XBOOLE_0:def 3;

then h . 2 = h . 3 by RELAT_1:def 10;

hence contradiction by A6, A8, A12, A17, A22, FUNCT_1:def 4; :: thesis: verum

[3,2] in the InternalRel of (Necklace 4) by ENUMSET1:def 4, NECKLA_2:2;

then [3,2] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A42, XBOOLE_0:def 4;

then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;

hence contradiction by Th12; :: thesis: verum

then A43: [(h . 2),(h . 0)] in the InternalRel of G by A9, A10, A17;

[0,2] in the InternalRel of (ComplRelStr (Necklace 4)) by Th11, ENUMSET1:def 4;

then A44: [(h . 0),(h . 2)] in the InternalRel of G by A9, A10, A17;

for x, y being Element of (Necklace 4) holds

( [x,y] in the InternalRel of (Necklace 4) iff [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) )

proof

hence
ComplRelStr G embeds Necklace 4
by A4, A1, A6, A8; :: thesis: verum
let x, y be Element of (Necklace 4); :: thesis: ( [x,y] in the InternalRel of (Necklace 4) iff [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) )

thus ( [x,y] in the InternalRel of (Necklace 4) implies [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) ) :: thesis: ( [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) implies [x,y] in the InternalRel of (Necklace 4) )

end;thus ( [x,y] in the InternalRel of (Necklace 4) implies [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) ) :: thesis: ( [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) implies [x,y] in the InternalRel of (Necklace 4) )

proof

assume A52:
[(h . x),(h . y)] in the InternalRel of (ComplRelStr G)
; :: thesis: [x,y] in the InternalRel of (Necklace 4)
assume A45:
[x,y] in the InternalRel of (Necklace 4)
; :: thesis: [(h . x),(h . y)] in the InternalRel of (ComplRelStr G)

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

end;

suppose A46:
[x,y] = [0,1]
; :: thesis: [(h . x),(h . y)] in the InternalRel of (ComplRelStr G)

then
x = 0
by XTUPLE_0:1;

hence [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) by A13, A46, XTUPLE_0:1; :: thesis: verum

end;hence [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) by A13, A46, XTUPLE_0:1; :: thesis: verum

suppose A47:
[x,y] = [1,0]
; :: thesis: [(h . x),(h . y)] in the InternalRel of (ComplRelStr G)

then
x = 1
by XTUPLE_0:1;

hence [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) by A31, A47, XTUPLE_0:1; :: thesis: verum

end;hence [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) by A31, A47, XTUPLE_0:1; :: thesis: verum

suppose A48:
[x,y] = [1,2]
; :: thesis: [(h . x),(h . y)] in the InternalRel of (ComplRelStr G)

then
x = 1
by XTUPLE_0:1;

hence [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) by A18, A48, XTUPLE_0:1; :: thesis: verum

end;hence [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) by A18, A48, XTUPLE_0:1; :: thesis: verum

suppose A49:
[x,y] = [2,1]
; :: thesis: [(h . x),(h . y)] in the InternalRel of (ComplRelStr G)

then
x = 2
by XTUPLE_0:1;

hence [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) by A35, A49, XTUPLE_0:1; :: thesis: verum

end;hence [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) by A35, A49, XTUPLE_0:1; :: thesis: verum

suppose A50:
[x,y] = [2,3]
; :: thesis: [(h . x),(h . y)] in the InternalRel of (ComplRelStr G)

then
x = 2
by XTUPLE_0:1;

hence [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) by A23, A50, XTUPLE_0:1; :: thesis: verum

end;hence [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) by A23, A50, XTUPLE_0:1; :: thesis: verum

suppose A51:
[x,y] = [3,2]
; :: thesis: [(h . x),(h . y)] in the InternalRel of (ComplRelStr G)

then
x = 3
by XTUPLE_0:1;

hence [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) by A39, A51, XTUPLE_0:1; :: thesis: verum

end;hence [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) by A39, A51, XTUPLE_0:1; :: thesis: verum

per cases
( ( x = 0 & y = 0 ) or ( x = 0 & y = 1 ) or ( x = 0 & y = 2 ) or ( x = 0 & y = 3 ) or ( x = 1 & y = 0 ) or ( x = 1 & y = 1 ) or ( x = 1 & y = 2 ) or ( x = 1 & y = 3 ) or ( x = 2 & y = 0 ) or ( x = 2 & y = 1 ) or ( x = 2 & y = 2 ) or ( x = 2 & y = 3 ) or ( x = 3 & y = 0 ) or ( x = 3 & y = 1 ) or ( x = 3 & y = 2 ) or ( x = 3 & y = 3 ) )
by A2, ENUMSET1:def 2;

end;

suppose A53:
( x = 0 & y = 0 )
; :: thesis: [x,y] in the InternalRel of (Necklace 4)

then
h . 0 in the carrier of (ComplRelStr G)
by A52, ZFMISC_1:87;

hence [x,y] in the InternalRel of (Necklace 4) by A52, A53, NECKLACE:def 5; :: thesis: verum

end;hence [x,y] in the InternalRel of (Necklace 4) by A52, A53, NECKLACE:def 5; :: thesis: verum

suppose
( x = 0 & y = 2 )
; :: thesis: [x,y] in the InternalRel of (Necklace 4)

then
[(h . 0),(h . 2)] in the InternalRel of G /\ the InternalRel of (ComplRelStr G)
by A44, A52, XBOOLE_0:def 4;

then the InternalRel of G meets the InternalRel of (ComplRelStr G) ;

hence [x,y] in the InternalRel of (Necklace 4) by Th12; :: thesis: verum

end;then the InternalRel of G meets the InternalRel of (ComplRelStr G) ;

hence [x,y] in the InternalRel of (Necklace 4) by Th12; :: thesis: verum

suppose
( x = 0 & y = 3 )
; :: thesis: [x,y] in the InternalRel of (Necklace 4)

then
[(h . 0),(h . 3)] in the InternalRel of G /\ the InternalRel of (ComplRelStr G)
by A30, A52, XBOOLE_0:def 4;

then the InternalRel of G meets the InternalRel of (ComplRelStr G) ;

hence [x,y] in the InternalRel of (Necklace 4) by Th12; :: thesis: verum

end;then the InternalRel of G meets the InternalRel of (ComplRelStr G) ;

hence [x,y] in the InternalRel of (Necklace 4) by Th12; :: thesis: verum

suppose A54:
( x = 1 & y = 1 )
; :: thesis: [x,y] in the InternalRel of (Necklace 4)

then
h . 1 in the carrier of (ComplRelStr G)
by A52, ZFMISC_1:87;

hence [x,y] in the InternalRel of (Necklace 4) by A52, A54, NECKLACE:def 5; :: thesis: verum

end;hence [x,y] in the InternalRel of (Necklace 4) by A52, A54, NECKLACE:def 5; :: thesis: verum

suppose
( x = 1 & y = 3 )
; :: thesis: [x,y] in the InternalRel of (Necklace 4)

then
[(h . 1),(h . 3)] in the InternalRel of G /\ the InternalRel of (ComplRelStr G)
by A28, A52, XBOOLE_0:def 4;

then the InternalRel of G meets the InternalRel of (ComplRelStr G) ;

hence [x,y] in the InternalRel of (Necklace 4) by Th12; :: thesis: verum

end;then the InternalRel of G meets the InternalRel of (ComplRelStr G) ;

hence [x,y] in the InternalRel of (Necklace 4) by Th12; :: thesis: verum

suppose
( x = 2 & y = 0 )
; :: thesis: [x,y] in the InternalRel of (Necklace 4)

then
[(h . 2),(h . 0)] in the InternalRel of G /\ the InternalRel of (ComplRelStr G)
by A43, A52, XBOOLE_0:def 4;

then the InternalRel of G meets the InternalRel of (ComplRelStr G) ;

hence [x,y] in the InternalRel of (Necklace 4) by Th12; :: thesis: verum

end;then the InternalRel of G meets the InternalRel of (ComplRelStr G) ;

hence [x,y] in the InternalRel of (Necklace 4) by Th12; :: thesis: verum

suppose A55:
( x = 2 & y = 2 )
; :: thesis: [x,y] in the InternalRel of (Necklace 4)

then
h . 2 in the carrier of (ComplRelStr G)
by A52, ZFMISC_1:87;

hence [x,y] in the InternalRel of (Necklace 4) by A52, A55, NECKLACE:def 5; :: thesis: verum

end;hence [x,y] in the InternalRel of (Necklace 4) by A52, A55, NECKLACE:def 5; :: thesis: verum

suppose
( x = 3 & y = 0 )
; :: thesis: [x,y] in the InternalRel of (Necklace 4)

then
[(h . 3),(h . 0)] in the InternalRel of G /\ the InternalRel of (ComplRelStr G)
by A29, A52, XBOOLE_0:def 4;

then the InternalRel of G meets the InternalRel of (ComplRelStr G) ;

hence [x,y] in the InternalRel of (Necklace 4) by Th12; :: thesis: verum

end;then the InternalRel of G meets the InternalRel of (ComplRelStr G) ;

hence [x,y] in the InternalRel of (Necklace 4) by Th12; :: thesis: verum

suppose
( x = 3 & y = 1 )
; :: thesis: [x,y] in the InternalRel of (Necklace 4)

then
[(h . 3),(h . 1)] in the InternalRel of G /\ the InternalRel of (ComplRelStr G)
by A27, A52, XBOOLE_0:def 4;

then the InternalRel of G meets the InternalRel of (ComplRelStr G) ;

hence [x,y] in the InternalRel of (Necklace 4) by Th12; :: thesis: verum

end;then the InternalRel of G meets the InternalRel of (ComplRelStr G) ;

hence [x,y] in the InternalRel of (Necklace 4) by Th12; :: thesis: verum

suppose A56:
( x = 3 & y = 3 )
; :: thesis: [x,y] in the InternalRel of (Necklace 4)

then
h . 3 in the carrier of (ComplRelStr G)
by A52, ZFMISC_1:87;

hence [x,y] in the InternalRel of (Necklace 4) by A52, A56, NECKLACE:def 5; :: thesis: verum

end;hence [x,y] in the InternalRel of (Necklace 4) by A52, A56, NECKLACE:def 5; :: thesis: verum

then consider f being Function of (Necklace 4),(ComplRelStr G) such that

A57: f is V24() and

A58: for x, y being Element of (Necklace 4) holds

( [x,y] in the InternalRel of (Necklace 4) iff [(f . x),(f . y)] in the InternalRel of (ComplRelStr G) ) ;

consider g being Function of (Necklace 4),(ComplRelStr (Necklace 4)) such that

A59: g is isomorphic by NECKLACE:29, WAYBEL_1:def 8;

A60: 2 in the carrier of (Necklace 4) by A2, ENUMSET1:def 2;

A61: dom f = the carrier of (Necklace 4) by FUNCT_2:def 1;

A62: [(f . 0),(f . 2)] in the InternalRel of G

proof

A66:
3 in the carrier of (Necklace 4)
by A2, ENUMSET1:def 2;
assume A63:
not [(f . 0),(f . 2)] in the InternalRel of G
; :: thesis: contradiction

[(f . 0),(f . 2)] in the InternalRel of (ComplRelStr G)

[0,2] in the InternalRel of (ComplRelStr (Necklace 4)) by Th11, ENUMSET1:def 4;

then [0,2] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A65, XBOOLE_0:def 4;

then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;

hence contradiction by Th12; :: thesis: verum

end;[(f . 0),(f . 2)] in the InternalRel of (ComplRelStr G)

proof

then A65:
[0,2] in the InternalRel of (Necklace 4)
by A58, A3, A60;
( f . 0 in the carrier of (ComplRelStr G) & f . 2 in the carrier of (ComplRelStr G) )
by A3, A60, FUNCT_2:5;

then [(f . 0),(f . 2)] in [: the carrier of G, the carrier of G:] by A1, ZFMISC_1:87;

then [(f . 0),(f . 2)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;

then A64: ( [(f . 0),(f . 2)] in (id the carrier of G) \/ the InternalRel of G or [(f . 0),(f . 2)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;

assume not [(f . 0),(f . 2)] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction

then [(f . 0),(f . 2)] in id the carrier of G by A63, A64, XBOOLE_0:def 3;

then f . 0 = f . 2 by RELAT_1:def 10;

hence contradiction by A57, A61, A3, A60, FUNCT_1:def 4; :: thesis: verum

end;then [(f . 0),(f . 2)] in [: the carrier of G, the carrier of G:] by A1, ZFMISC_1:87;

then [(f . 0),(f . 2)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;

then A64: ( [(f . 0),(f . 2)] in (id the carrier of G) \/ the InternalRel of G or [(f . 0),(f . 2)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;

assume not [(f . 0),(f . 2)] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction

then [(f . 0),(f . 2)] in id the carrier of G by A63, A64, XBOOLE_0:def 3;

then f . 0 = f . 2 by RELAT_1:def 10;

hence contradiction by A57, A61, A3, A60, FUNCT_1:def 4; :: thesis: verum

[0,2] in the InternalRel of (ComplRelStr (Necklace 4)) by Th11, ENUMSET1:def 4;

then [0,2] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A65, XBOOLE_0:def 4;

then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;

hence contradiction by Th12; :: thesis: verum

A67: [(f . 0),(f . 3)] in the InternalRel of G

proof

A71:
1 in the carrier of (Necklace 4)
by A2, ENUMSET1:def 2;
assume A68:
not [(f . 0),(f . 3)] in the InternalRel of G
; :: thesis: contradiction

[(f . 0),(f . 3)] in the InternalRel of (ComplRelStr G)

[0,3] in the InternalRel of (ComplRelStr (Necklace 4)) by Th11, ENUMSET1:def 4;

then [0,3] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A70, XBOOLE_0:def 4;

then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;

hence contradiction by Th12; :: thesis: verum

end;[(f . 0),(f . 3)] in the InternalRel of (ComplRelStr G)

proof

then A70:
[0,3] in the InternalRel of (Necklace 4)
by A58, A3, A66;
( f . 0 in the carrier of (ComplRelStr G) & f . 3 in the carrier of (ComplRelStr G) )
by A3, A66, FUNCT_2:5;

then [(f . 0),(f . 3)] in [: the carrier of G, the carrier of G:] by A1, ZFMISC_1:87;

then [(f . 0),(f . 3)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;

then A69: ( [(f . 0),(f . 3)] in (id the carrier of G) \/ the InternalRel of G or [(f . 0),(f . 3)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;

assume not [(f . 0),(f . 3)] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction

then [(f . 0),(f . 3)] in id the carrier of G by A68, A69, XBOOLE_0:def 3;

then f . 0 = f . 3 by RELAT_1:def 10;

hence contradiction by A57, A61, A3, A66, FUNCT_1:def 4; :: thesis: verum

end;then [(f . 0),(f . 3)] in [: the carrier of G, the carrier of G:] by A1, ZFMISC_1:87;

then [(f . 0),(f . 3)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;

then A69: ( [(f . 0),(f . 3)] in (id the carrier of G) \/ the InternalRel of G or [(f . 0),(f . 3)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;

assume not [(f . 0),(f . 3)] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction

then [(f . 0),(f . 3)] in id the carrier of G by A68, A69, XBOOLE_0:def 3;

then f . 0 = f . 3 by RELAT_1:def 10;

hence contradiction by A57, A61, A3, A66, FUNCT_1:def 4; :: thesis: verum

[0,3] in the InternalRel of (ComplRelStr (Necklace 4)) by Th11, ENUMSET1:def 4;

then [0,3] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A70, XBOOLE_0:def 4;

then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;

hence contradiction by Th12; :: thesis: verum

A72: [(f . 1),(f . 3)] in the InternalRel of G

proof

[3,2] in the InternalRel of (Necklace 4)
by ENUMSET1:def 4, NECKLA_2:2;
assume A73:
not [(f . 1),(f . 3)] in the InternalRel of G
; :: thesis: contradiction

[(f . 1),(f . 3)] in the InternalRel of (ComplRelStr G)

[1,3] in the InternalRel of (ComplRelStr (Necklace 4)) by Th11, ENUMSET1:def 4;

then [1,3] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A75, XBOOLE_0:def 4;

then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;

hence contradiction by Th12; :: thesis: verum

end;[(f . 1),(f . 3)] in the InternalRel of (ComplRelStr G)

proof

then A75:
[1,3] in the InternalRel of (Necklace 4)
by A58, A71, A66;
( f . 1 in the carrier of (ComplRelStr G) & f . 3 in the carrier of (ComplRelStr G) )
by A71, A66, FUNCT_2:5;

then [(f . 1),(f . 3)] in [: the carrier of G, the carrier of G:] by A1, ZFMISC_1:87;

then [(f . 1),(f . 3)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;

then A74: ( [(f . 1),(f . 3)] in (id the carrier of G) \/ the InternalRel of G or [(f . 1),(f . 3)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;

assume not [(f . 1),(f . 3)] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction

then [(f . 1),(f . 3)] in id the carrier of G by A73, A74, XBOOLE_0:def 3;

then f . 1 = f . 3 by RELAT_1:def 10;

hence contradiction by A57, A61, A71, A66, FUNCT_1:def 4; :: thesis: verum

end;then [(f . 1),(f . 3)] in [: the carrier of G, the carrier of G:] by A1, ZFMISC_1:87;

then [(f . 1),(f . 3)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;

then A74: ( [(f . 1),(f . 3)] in (id the carrier of G) \/ the InternalRel of G or [(f . 1),(f . 3)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;

assume not [(f . 1),(f . 3)] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction

then [(f . 1),(f . 3)] in id the carrier of G by A73, A74, XBOOLE_0:def 3;

then f . 1 = f . 3 by RELAT_1:def 10;

hence contradiction by A57, A61, A71, A66, FUNCT_1:def 4; :: thesis: verum

[1,3] in the InternalRel of (ComplRelStr (Necklace 4)) by Th11, ENUMSET1:def 4;

then [1,3] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A75, XBOOLE_0:def 4;

then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;

hence contradiction by Th12; :: thesis: verum

then A76: [(f . 3),(f . 2)] in the InternalRel of (ComplRelStr G) by A58, A60, A66;

[2,3] in the InternalRel of (Necklace 4) by ENUMSET1:def 4, NECKLA_2:2;

then A77: [(f . 2),(f . 3)] in the InternalRel of (ComplRelStr G) by A58, A60, A66;

[1,2] in the InternalRel of (Necklace 4) by ENUMSET1:def 4, NECKLA_2:2;

then A78: [(f . 1),(f . 2)] in the InternalRel of (ComplRelStr G) by A58, A71, A60;

[1,0] in the InternalRel of (Necklace 4) by ENUMSET1:def 4, NECKLA_2:2;

then A79: [(f . 1),(f . 0)] in the InternalRel of (ComplRelStr G) by A58, A3, A71;

A80: [(f . 2),(f . 0)] in the InternalRel of G

proof

A84:
[(f . 3),(f . 0)] in the InternalRel of G
assume A81:
not [(f . 2),(f . 0)] in the InternalRel of G
; :: thesis: contradiction

[(f . 2),(f . 0)] in the InternalRel of (ComplRelStr G)

[2,0] in the InternalRel of (ComplRelStr (Necklace 4)) by Th11, ENUMSET1:def 4;

then [2,0] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A83, XBOOLE_0:def 4;

then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;

hence contradiction by Th12; :: thesis: verum

end;[(f . 2),(f . 0)] in the InternalRel of (ComplRelStr G)

proof

then A83:
[2,0] in the InternalRel of (Necklace 4)
by A58, A3, A60;
( f . 0 in the carrier of (ComplRelStr G) & f . 2 in the carrier of (ComplRelStr G) )
by A3, A60, FUNCT_2:5;

then [(f . 2),(f . 0)] in [: the carrier of G, the carrier of G:] by A1, ZFMISC_1:87;

then [(f . 2),(f . 0)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;

then A82: ( [(f . 2),(f . 0)] in (id the carrier of G) \/ the InternalRel of G or [(f . 2),(f . 0)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;

assume not [(f . 2),(f . 0)] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction

then [(f . 2),(f . 0)] in id the carrier of G by A81, A82, XBOOLE_0:def 3;

then f . 0 = f . 2 by RELAT_1:def 10;

hence contradiction by A57, A61, A3, A60, FUNCT_1:def 4; :: thesis: verum

end;then [(f . 2),(f . 0)] in [: the carrier of G, the carrier of G:] by A1, ZFMISC_1:87;

then [(f . 2),(f . 0)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;

then A82: ( [(f . 2),(f . 0)] in (id the carrier of G) \/ the InternalRel of G or [(f . 2),(f . 0)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;

assume not [(f . 2),(f . 0)] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction

then [(f . 2),(f . 0)] in id the carrier of G by A81, A82, XBOOLE_0:def 3;

then f . 0 = f . 2 by RELAT_1:def 10;

hence contradiction by A57, A61, A3, A60, FUNCT_1:def 4; :: thesis: verum

[2,0] in the InternalRel of (ComplRelStr (Necklace 4)) by Th11, ENUMSET1:def 4;

then [2,0] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A83, XBOOLE_0:def 4;

then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;

hence contradiction by Th12; :: thesis: verum

proof

A88:
[(f . 3),(f . 1)] in the InternalRel of G
assume A85:
not [(f . 3),(f . 0)] in the InternalRel of G
; :: thesis: contradiction

[(f . 3),(f . 0)] in the InternalRel of (ComplRelStr G)

[3,0] in the InternalRel of (ComplRelStr (Necklace 4)) by Th11, ENUMSET1:def 4;

then [3,0] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A87, XBOOLE_0:def 4;

then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;

hence contradiction by Th12; :: thesis: verum

end;[(f . 3),(f . 0)] in the InternalRel of (ComplRelStr G)

proof

then A87:
[3,0] in the InternalRel of (Necklace 4)
by A58, A3, A66;
( f . 0 in the carrier of (ComplRelStr G) & f . 3 in the carrier of (ComplRelStr G) )
by A3, A66, FUNCT_2:5;

then [(f . 3),(f . 0)] in [: the carrier of G, the carrier of G:] by A1, ZFMISC_1:87;

then [(f . 3),(f . 0)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;

then A86: ( [(f . 3),(f . 0)] in (id the carrier of G) \/ the InternalRel of G or [(f . 3),(f . 0)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;

assume not [(f . 3),(f . 0)] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction

then [(f . 3),(f . 0)] in id the carrier of G by A85, A86, XBOOLE_0:def 3;

then f . 0 = f . 3 by RELAT_1:def 10;

hence contradiction by A57, A61, A3, A66, FUNCT_1:def 4; :: thesis: verum

end;then [(f . 3),(f . 0)] in [: the carrier of G, the carrier of G:] by A1, ZFMISC_1:87;

then [(f . 3),(f . 0)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;

then A86: ( [(f . 3),(f . 0)] in (id the carrier of G) \/ the InternalRel of G or [(f . 3),(f . 0)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;

assume not [(f . 3),(f . 0)] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction

then [(f . 3),(f . 0)] in id the carrier of G by A85, A86, XBOOLE_0:def 3;

then f . 0 = f . 3 by RELAT_1:def 10;

hence contradiction by A57, A61, A3, A66, FUNCT_1:def 4; :: thesis: verum

[3,0] in the InternalRel of (ComplRelStr (Necklace 4)) by Th11, ENUMSET1:def 4;

then [3,0] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A87, XBOOLE_0:def 4;

then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;

hence contradiction by Th12; :: thesis: verum

proof

[2,1] in the InternalRel of (Necklace 4)
by ENUMSET1:def 4, NECKLA_2:2;
assume A89:
not [(f . 3),(f . 1)] in the InternalRel of G
; :: thesis: contradiction

[(f . 3),(f . 1)] in the InternalRel of (ComplRelStr G)

[3,1] in the InternalRel of (ComplRelStr (Necklace 4)) by Th11, ENUMSET1:def 4;

then [3,1] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A91, XBOOLE_0:def 4;

then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;

hence contradiction by Th12; :: thesis: verum

end;[(f . 3),(f . 1)] in the InternalRel of (ComplRelStr G)

proof

then A91:
[3,1] in the InternalRel of (Necklace 4)
by A58, A71, A66;
( f . 1 in the carrier of (ComplRelStr G) & f . 3 in the carrier of (ComplRelStr G) )
by A71, A66, FUNCT_2:5;

then [(f . 3),(f . 1)] in [: the carrier of G, the carrier of G:] by A1, ZFMISC_1:87;

then [(f . 3),(f . 1)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;

then A90: ( [(f . 3),(f . 1)] in (id the carrier of G) \/ the InternalRel of G or [(f . 3),(f . 1)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;

assume not [(f . 3),(f . 1)] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction

then [(f . 3),(f . 1)] in id the carrier of G by A89, A90, XBOOLE_0:def 3;

then f . 1 = f . 3 by RELAT_1:def 10;

hence contradiction by A57, A61, A71, A66, FUNCT_1:def 4; :: thesis: verum

end;then [(f . 3),(f . 1)] in [: the carrier of G, the carrier of G:] by A1, ZFMISC_1:87;

then [(f . 3),(f . 1)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;

then A90: ( [(f . 3),(f . 1)] in (id the carrier of G) \/ the InternalRel of G or [(f . 3),(f . 1)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;

assume not [(f . 3),(f . 1)] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction

then [(f . 3),(f . 1)] in id the carrier of G by A89, A90, XBOOLE_0:def 3;

then f . 1 = f . 3 by RELAT_1:def 10;

hence contradiction by A57, A61, A71, A66, FUNCT_1:def 4; :: thesis: verum

[3,1] in the InternalRel of (ComplRelStr (Necklace 4)) by Th11, ENUMSET1:def 4;

then [3,1] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A91, XBOOLE_0:def 4;

then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;

hence contradiction by Th12; :: thesis: verum

then A92: [(f . 2),(f . 1)] in the InternalRel of (ComplRelStr G) by A58, A71, A60;

[0,1] in the InternalRel of (Necklace 4) by ENUMSET1:def 4, NECKLA_2:2;

then A93: [(f . 0),(f . 1)] in the InternalRel of (ComplRelStr G) by A58, A3, A71;

A94: for x, y being Element of (ComplRelStr (Necklace 4)) holds

( [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) iff [(f . x),(f . y)] in the InternalRel of G )

proof

reconsider f = f as Function of (ComplRelStr (Necklace 4)),G by A4, NECKLACE:def 8;
let x, y be Element of (ComplRelStr (Necklace 4)); :: thesis: ( [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) iff [(f . x),(f . y)] in the InternalRel of G )

A95: the carrier of (Necklace 4) = the carrier of (ComplRelStr (Necklace 4)) by NECKLACE:def 8;

thus ( [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) implies [(f . x),(f . y)] in the InternalRel of G ) :: thesis: ( [(f . x),(f . y)] in the InternalRel of G implies [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) )

end;A95: the carrier of (Necklace 4) = the carrier of (ComplRelStr (Necklace 4)) by NECKLACE:def 8;

thus ( [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) implies [(f . x),(f . y)] in the InternalRel of G ) :: thesis: ( [(f . x),(f . y)] in the InternalRel of G implies [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) )

proof

assume A103:
[(f . x),(f . y)] in the InternalRel of G
; :: thesis: [x,y] in the InternalRel of (ComplRelStr (Necklace 4))
assume A96:
[x,y] in the InternalRel of (ComplRelStr (Necklace 4))
; :: thesis: [(f . x),(f . y)] in the InternalRel of G

end;per cases
( [x,y] = [0,2] or [x,y] = [2,0] or [x,y] = [0,3] or [x,y] = [3,0] or [x,y] = [1,3] or [x,y] = [3,1] )
by A96, Th11, ENUMSET1:def 4;

end;

suppose A97:
[x,y] = [0,2]
; :: thesis: [(f . x),(f . y)] in the InternalRel of G

then
x = 0
by XTUPLE_0:1;

hence [(f . x),(f . y)] in the InternalRel of G by A62, A97, XTUPLE_0:1; :: thesis: verum

end;hence [(f . x),(f . y)] in the InternalRel of G by A62, A97, XTUPLE_0:1; :: thesis: verum

suppose A98:
[x,y] = [2,0]
; :: thesis: [(f . x),(f . y)] in the InternalRel of G

then
x = 2
by XTUPLE_0:1;

hence [(f . x),(f . y)] in the InternalRel of G by A80, A98, XTUPLE_0:1; :: thesis: verum

end;hence [(f . x),(f . y)] in the InternalRel of G by A80, A98, XTUPLE_0:1; :: thesis: verum

suppose A99:
[x,y] = [0,3]
; :: thesis: [(f . x),(f . y)] in the InternalRel of G

then
x = 0
by XTUPLE_0:1;

hence [(f . x),(f . y)] in the InternalRel of G by A67, A99, XTUPLE_0:1; :: thesis: verum

end;hence [(f . x),(f . y)] in the InternalRel of G by A67, A99, XTUPLE_0:1; :: thesis: verum

suppose A100:
[x,y] = [3,0]
; :: thesis: [(f . x),(f . y)] in the InternalRel of G

then
x = 3
by XTUPLE_0:1;

hence [(f . x),(f . y)] in the InternalRel of G by A84, A100, XTUPLE_0:1; :: thesis: verum

end;hence [(f . x),(f . y)] in the InternalRel of G by A84, A100, XTUPLE_0:1; :: thesis: verum

suppose A101:
[x,y] = [1,3]
; :: thesis: [(f . x),(f . y)] in the InternalRel of G

then
x = 1
by XTUPLE_0:1;

hence [(f . x),(f . y)] in the InternalRel of G by A72, A101, XTUPLE_0:1; :: thesis: verum

end;hence [(f . x),(f . y)] in the InternalRel of G by A72, A101, XTUPLE_0:1; :: thesis: verum

suppose A102:
[x,y] = [3,1]
; :: thesis: [(f . x),(f . y)] in the InternalRel of G

then
x = 3
by XTUPLE_0:1;

hence [(f . x),(f . y)] in the InternalRel of G by A88, A102, XTUPLE_0:1; :: thesis: verum

end;hence [(f . x),(f . y)] in the InternalRel of G by A88, A102, XTUPLE_0:1; :: thesis: verum

per cases
( ( x = 0 & y = 0 ) or ( x = 0 & y = 1 ) or ( x = 0 & y = 2 ) or ( x = 0 & y = 3 ) or ( x = 1 & y = 0 ) or ( x = 2 & y = 0 ) or ( x = 3 & y = 0 ) or ( x = 1 & y = 1 ) or ( x = 1 & y = 2 ) or ( x = 1 & y = 3 ) or ( x = 2 & y = 1 ) or ( x = 2 & y = 2 ) or ( x = 2 & y = 3 ) or ( x = 3 & y = 1 ) or ( x = 3 & y = 2 ) or ( x = 3 & y = 3 ) )
by A2, A95, ENUMSET1:def 2;

end;

suppose A104:
( x = 0 & y = 0 )
; :: thesis: [x,y] in the InternalRel of (ComplRelStr (Necklace 4))

then
f . 0 in the carrier of G
by A103, ZFMISC_1:87;

hence [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) by A103, A104, NECKLACE:def 5; :: thesis: verum

end;hence [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) by A103, A104, NECKLACE:def 5; :: thesis: verum

suppose
( x = 0 & y = 1 )
; :: thesis: [x,y] in the InternalRel of (ComplRelStr (Necklace 4))

then
[(f . 0),(f . 1)] in the InternalRel of G /\ the InternalRel of (ComplRelStr G)
by A93, A103, XBOOLE_0:def 4;

then the InternalRel of G meets the InternalRel of (ComplRelStr G) ;

hence [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) by Th12; :: thesis: verum

end;then the InternalRel of G meets the InternalRel of (ComplRelStr G) ;

hence [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) by Th12; :: thesis: verum

suppose
( x = 0 & y = 2 )
; :: thesis: [x,y] in the InternalRel of (ComplRelStr (Necklace 4))

hence
[x,y] in the InternalRel of (ComplRelStr (Necklace 4))
by Th11, ENUMSET1:def 4; :: thesis: verum

end;suppose
( x = 0 & y = 3 )
; :: thesis: [x,y] in the InternalRel of (ComplRelStr (Necklace 4))

hence
[x,y] in the InternalRel of (ComplRelStr (Necklace 4))
by Th11, ENUMSET1:def 4; :: thesis: verum

end;suppose
( x = 1 & y = 0 )
; :: thesis: [x,y] in the InternalRel of (ComplRelStr (Necklace 4))

then
[(f . 1),(f . 0)] in the InternalRel of G /\ the InternalRel of (ComplRelStr G)
by A79, A103, XBOOLE_0:def 4;

then the InternalRel of G meets the InternalRel of (ComplRelStr G) ;

hence [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) by Th12; :: thesis: verum

end;then the InternalRel of G meets the InternalRel of (ComplRelStr G) ;

hence [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) by Th12; :: thesis: verum

suppose
( x = 2 & y = 0 )
; :: thesis: [x,y] in the InternalRel of (ComplRelStr (Necklace 4))

hence
[x,y] in the InternalRel of (ComplRelStr (Necklace 4))
by Th11, ENUMSET1:def 4; :: thesis: verum

end;suppose
( x = 3 & y = 0 )
; :: thesis: [x,y] in the InternalRel of (ComplRelStr (Necklace 4))

hence
[x,y] in the InternalRel of (ComplRelStr (Necklace 4))
by Th11, ENUMSET1:def 4; :: thesis: verum

end;

suppose A105:
( x = 1 & y = 1 )
; :: thesis: [x,y] in the InternalRel of (ComplRelStr (Necklace 4))

then
f . 1 in the carrier of G
by A103, ZFMISC_1:87;

hence [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) by A103, A105, NECKLACE:def 5; :: thesis: verum

end;hence [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) by A103, A105, NECKLACE:def 5; :: thesis: verum

suppose
( x = 1 & y = 2 )
; :: thesis: [x,y] in the InternalRel of (ComplRelStr (Necklace 4))

then
[(f . 1),(f . 2)] in the InternalRel of G /\ the InternalRel of (ComplRelStr G)
by A78, A103, XBOOLE_0:def 4;

then the InternalRel of G meets the InternalRel of (ComplRelStr G) ;

hence [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) by Th12; :: thesis: verum

end;then the InternalRel of G meets the InternalRel of (ComplRelStr G) ;

hence [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) by Th12; :: thesis: verum

suppose
( x = 1 & y = 3 )
; :: thesis: [x,y] in the InternalRel of (ComplRelStr (Necklace 4))

hence
[x,y] in the InternalRel of (ComplRelStr (Necklace 4))
by Th11, ENUMSET1:def 4; :: thesis: verum

end;

suppose
( x = 2 & y = 1 )
; :: thesis: [x,y] in the InternalRel of (ComplRelStr (Necklace 4))

then
[(f . 2),(f . 1)] in the InternalRel of G /\ the InternalRel of (ComplRelStr G)
by A92, A103, XBOOLE_0:def 4;

then the InternalRel of G meets the InternalRel of (ComplRelStr G) ;

hence [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) by Th12; :: thesis: verum

end;then the InternalRel of G meets the InternalRel of (ComplRelStr G) ;

hence [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) by Th12; :: thesis: verum

suppose A106:
( x = 2 & y = 2 )
; :: thesis: [x,y] in the InternalRel of (ComplRelStr (Necklace 4))

then
f . 2 in the carrier of G
by A103, ZFMISC_1:87;

hence [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) by A103, A106, NECKLACE:def 5; :: thesis: verum

end;hence [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) by A103, A106, NECKLACE:def 5; :: thesis: verum

suppose
( x = 2 & y = 3 )
; :: thesis: [x,y] in the InternalRel of (ComplRelStr (Necklace 4))

then
[(f . 2),(f . 3)] in the InternalRel of G /\ the InternalRel of (ComplRelStr G)
by A77, A103, XBOOLE_0:def 4;

then the InternalRel of G meets the InternalRel of (ComplRelStr G) ;

hence [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) by Th12; :: thesis: verum

end;then the InternalRel of G meets the InternalRel of (ComplRelStr G) ;

hence [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) by Th12; :: thesis: verum

suppose
( x = 3 & y = 1 )
; :: thesis: [x,y] in the InternalRel of (ComplRelStr (Necklace 4))

hence
[x,y] in the InternalRel of (ComplRelStr (Necklace 4))
by Th11, ENUMSET1:def 4; :: thesis: verum

end;

suppose
( x = 3 & y = 2 )
; :: thesis: [x,y] in the InternalRel of (ComplRelStr (Necklace 4))

then
[(f . 3),(f . 2)] in the InternalRel of G /\ the InternalRel of (ComplRelStr G)
by A76, A103, XBOOLE_0:def 4;

then the InternalRel of G meets the InternalRel of (ComplRelStr G) ;

hence [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) by Th12; :: thesis: verum

end;then the InternalRel of G meets the InternalRel of (ComplRelStr G) ;

hence [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) by Th12; :: thesis: verum

suppose A107:
( x = 3 & y = 3 )
; :: thesis: [x,y] in the InternalRel of (ComplRelStr (Necklace 4))

then
f . 3 in the carrier of G
by A103, ZFMISC_1:87;

hence [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) by A103, A107, NECKLACE:def 5; :: thesis: verum

end;hence [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) by A103, A107, NECKLACE:def 5; :: thesis: verum

reconsider h = f * g as Function of (Necklace 4),G ;

A108: ( g is V24() & g is monotone ) by A59, WAYBEL_0:def 38;

for x, y being Element of (Necklace 4) holds

( [x,y] in the InternalRel of (Necklace 4) iff [(h . x),(h . y)] in the InternalRel of G )

proof

hence
G embeds Necklace 4
by A57, A108; :: thesis: verum
let x, y be Element of (Necklace 4); :: thesis: ( [x,y] in the InternalRel of (Necklace 4) iff [(h . x),(h . y)] in the InternalRel of G )

thus ( [x,y] in the InternalRel of (Necklace 4) implies [(h . x),(h . y)] in the InternalRel of G ) :: thesis: ( [(h . x),(h . y)] in the InternalRel of G implies [x,y] in the InternalRel of (Necklace 4) )

then [(f . (g . x)),(h . y)] in the InternalRel of G by FUNCT_2:15;

then [(f . (g . x)),(f . (g . y))] in the InternalRel of G by FUNCT_2:15;

then [(g . x),(g . y)] in the InternalRel of (ComplRelStr (Necklace 4)) by A94;

then g . x <= g . y by ORDERS_2:def 5;

then x <= y by A59, WAYBEL_0:66;

hence [x,y] in the InternalRel of (Necklace 4) by ORDERS_2:def 5; :: thesis: verum

end;thus ( [x,y] in the InternalRel of (Necklace 4) implies [(h . x),(h . y)] in the InternalRel of G ) :: thesis: ( [(h . x),(h . y)] in the InternalRel of G implies [x,y] in the InternalRel of (Necklace 4) )

proof

assume
[(h . x),(h . y)] in the InternalRel of G
; :: thesis: [x,y] in the InternalRel of (Necklace 4)
assume
[x,y] in the InternalRel of (Necklace 4)
; :: thesis: [(h . x),(h . y)] in the InternalRel of G

then x <= y by ORDERS_2:def 5;

then g . x <= g . y by A108, WAYBEL_1:def 2;

then [(g . x),(g . y)] in the InternalRel of (ComplRelStr (Necklace 4)) by ORDERS_2:def 5;

then [(f . (g . x)),(f . (g . y))] in the InternalRel of G by A94;

then [((f * g) . x),(f . (g . y))] in the InternalRel of G by FUNCT_2:15;

hence [(h . x),(h . y)] in the InternalRel of G by FUNCT_2:15; :: thesis: verum

end;then x <= y by ORDERS_2:def 5;

then g . x <= g . y by A108, WAYBEL_1:def 2;

then [(g . x),(g . y)] in the InternalRel of (ComplRelStr (Necklace 4)) by ORDERS_2:def 5;

then [(f . (g . x)),(f . (g . y))] in the InternalRel of G by A94;

then [((f * g) . x),(f . (g . y))] in the InternalRel of G by FUNCT_2:15;

hence [(h . x),(h . y)] in the InternalRel of G by FUNCT_2:15; :: thesis: verum

then [(f . (g . x)),(h . y)] in the InternalRel of G by FUNCT_2:15;

then [(f . (g . x)),(f . (g . y))] in the InternalRel of G by FUNCT_2:15;

then [(g . x),(g . y)] in the InternalRel of (ComplRelStr (Necklace 4)) by A94;

then g . x <= g . y by ORDERS_2:def 5;

then x <= y by A59, WAYBEL_0:66;

hence [x,y] in the InternalRel of (Necklace 4) by ORDERS_2:def 5; :: thesis: verum