let G be non empty irreflexive RelStr ; for x being Element of G
for x9 being Element of (ComplRelStr G) st x = x9 holds
ComplRelStr (subrelstr (([#] G) \ {x})) = subrelstr (([#] (ComplRelStr G)) \ {x9})
let x be Element of G; for x9 being Element of (ComplRelStr G) st x = x9 holds
ComplRelStr (subrelstr (([#] G) \ {x})) = subrelstr (([#] (ComplRelStr G)) \ {x9})
let x9 be Element of (ComplRelStr G); ( x = x9 implies ComplRelStr (subrelstr (([#] G) \ {x})) = subrelstr (([#] (ComplRelStr G)) \ {x9}) )
assume A1:
x = x9
; ComplRelStr (subrelstr (([#] G) \ {x})) = subrelstr (([#] (ComplRelStr G)) \ {x9})
set R = subrelstr (([#] G) \ {x});
set cR = the carrier of (subrelstr (([#] G) \ {x}));
set cG = the carrier of G;
A2:
[#] (ComplRelStr G) = the carrier of G
by NECKLACE:def 8;
A3: [:( the carrier of G \ {x}),( the carrier of G \ {x}):] =
[: the carrier of (subrelstr (([#] G) \ {x})),(([#] G) \ {x}):]
by YELLOW_0:def 15
.=
[: the carrier of (subrelstr (([#] G) \ {x})), the carrier of (subrelstr (([#] G) \ {x})):]
by YELLOW_0:def 15
;
A4:
the carrier of (subrelstr (([#] G) \ {x})) c= the carrier of G
by YELLOW_0:def 13;
A5: the InternalRel of (subrelstr (([#] (ComplRelStr G)) \ {x9})) =
the InternalRel of (ComplRelStr G) |_2 the carrier of (subrelstr (([#] (ComplRelStr G)) \ {x9}))
by YELLOW_0:def 14
.=
the InternalRel of (ComplRelStr G) |_2 ( the carrier of G \ {x})
by A1, A2, YELLOW_0:def 15
.=
(( the InternalRel of G `) \ (id the carrier of G)) /\ [:( the carrier of G \ {x}),( the carrier of G \ {x}):]
by NECKLACE:def 8
.=
([: the carrier of (subrelstr (([#] G) \ {x})), the carrier of (subrelstr (([#] G) \ {x})):] /\ ( the InternalRel of G `)) \ (id the carrier of G)
by A3, XBOOLE_1:49
.=
([: the carrier of (subrelstr (([#] G) \ {x})), the carrier of (subrelstr (([#] G) \ {x})):] /\ ([: the carrier of G, the carrier of G:] \ the InternalRel of G)) \ (id the carrier of G)
by SUBSET_1:def 4
.=
(([: the carrier of (subrelstr (([#] G) \ {x})), the carrier of (subrelstr (([#] G) \ {x})):] /\ [: the carrier of G, the carrier of G:]) \ the InternalRel of G) \ (id the carrier of G)
by XBOOLE_1:49
.=
([: the carrier of (subrelstr (([#] G) \ {x})), the carrier of (subrelstr (([#] G) \ {x})):] \ the InternalRel of G) \ (id the carrier of G)
by A4, XBOOLE_1:28, ZFMISC_1:96
;
A6: the InternalRel of (ComplRelStr (subrelstr (([#] G) \ {x}))) =
( the InternalRel of (subrelstr (([#] G) \ {x})) `) \ (id the carrier of (subrelstr (([#] G) \ {x})))
by NECKLACE:def 8
.=
([: the carrier of (subrelstr (([#] G) \ {x})), the carrier of (subrelstr (([#] G) \ {x})):] \ the InternalRel of (subrelstr (([#] G) \ {x}))) \ (id the carrier of (subrelstr (([#] G) \ {x})))
by SUBSET_1:def 4
.=
([: the carrier of (subrelstr (([#] G) \ {x})), the carrier of (subrelstr (([#] G) \ {x})):] \ ( the InternalRel of G |_2 the carrier of (subrelstr (([#] G) \ {x})))) \ (id the carrier of (subrelstr (([#] G) \ {x})))
by YELLOW_0:def 14
.=
(([: the carrier of (subrelstr (([#] G) \ {x})), the carrier of (subrelstr (([#] G) \ {x})):] \ the InternalRel of G) \/ ([: the carrier of (subrelstr (([#] G) \ {x})), the carrier of (subrelstr (([#] G) \ {x})):] \ [: the carrier of (subrelstr (([#] G) \ {x})), the carrier of (subrelstr (([#] G) \ {x})):])) \ (id the carrier of (subrelstr (([#] G) \ {x})))
by XBOOLE_1:54
.=
(([: the carrier of (subrelstr (([#] G) \ {x})), the carrier of (subrelstr (([#] G) \ {x})):] \ the InternalRel of G) \/ {}) \ (id the carrier of (subrelstr (([#] G) \ {x})))
by XBOOLE_1:37
.=
([: the carrier of (subrelstr (([#] G) \ {x})), the carrier of (subrelstr (([#] G) \ {x})):] \ the InternalRel of G) \ (id the carrier of (subrelstr (([#] G) \ {x})))
;
A7: [: the carrier of (subrelstr (([#] G) \ {x})), the carrier of (subrelstr (([#] G) \ {x})):] =
[:([#] G),(([#] G) \ {x}):] \ [:{x},(([#] G) \ {x}):]
by A3, ZFMISC_1:102
.=
([:([#] G),([#] G):] \ [:([#] G),{x}:]) \ [:{x},(([#] G) \ {x}):]
by ZFMISC_1:102
.=
([: the carrier of G, the carrier of G:] \ [: the carrier of G,{x}:]) \ ([:{x}, the carrier of G:] \ [:{x},{x}:])
by ZFMISC_1:102
.=
(([: the carrier of G, the carrier of G:] \ [: the carrier of G,{x}:]) \ [:{x}, the carrier of G:]) \/ (([: the carrier of G, the carrier of G:] \ [: the carrier of G,{x}:]) /\ [:{x},{x}:])
by XBOOLE_1:52
.=
([: the carrier of G, the carrier of G:] \ ([: the carrier of G,{x}:] \/ [:{x}, the carrier of G:])) \/ (([: the carrier of G, the carrier of G:] \ [: the carrier of G,{x}:]) /\ [:{x},{x}:])
by XBOOLE_1:41
;
A8:
the InternalRel of (subrelstr (([#] (ComplRelStr G)) \ {x9})) = the InternalRel of (ComplRelStr (subrelstr (([#] G) \ {x})))
the carrier of (ComplRelStr (subrelstr (([#] G) \ {x}))) =
the carrier of (subrelstr (([#] G) \ {x}))
by NECKLACE:def 8
.=
the carrier of G \ {x}
by YELLOW_0:def 15
.=
([#] (ComplRelStr G)) \ {x9}
by A1, NECKLACE:def 8
.=
the carrier of (subrelstr (([#] (ComplRelStr G)) \ {x9}))
by YELLOW_0:def 15
;
hence
ComplRelStr (subrelstr (([#] G) \ {x})) = subrelstr (([#] (ComplRelStr G)) \ {x9})
by A8; verum