let G be non empty irreflexive RelStr ; :: thesis: 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; :: thesis: 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); :: thesis: ( x = x9 implies ComplRelStr (subrelstr (([#] G) \ {x})) = subrelstr (([#] (ComplRelStr G)) \ {x9}) )
assume A1: x = x9 ; :: thesis: 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})))

proof

thus the InternalRel of (subrelstr (([#] (ComplRelStr G)) \ {x9})) c= the InternalRel of (ComplRelStr (subrelstr (([#] G) \ {x}))) :: according to XBOOLE_0:def 10 :: thesis: the InternalRel of (ComplRelStr (subrelstr (([#] G) \ {x}))) c= the InternalRel of (subrelstr (([#] (ComplRelStr G)) \ {x9}))

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the InternalRel of (subrelstr (([#] (ComplRelStr G)) \ {x9})) or a in the InternalRel of (ComplRelStr (subrelstr (([#] G) \ {x}))) )
assume A9: a in the InternalRel of (subrelstr (([#] (ComplRelStr G)) \ {x9})) ; :: thesis: a in the InternalRel of (ComplRelStr (subrelstr (([#] G) \ {x})))
then A10: not a in id the carrier of G by A5, XBOOLE_0:def 5;
A11: not a in id the carrier of (subrelstr (([#] G) \ {x}))

proof

assume A12: a in id the carrier of (subrelstr (([#] G) \ {x})) ; :: thesis: contradiction
then consider x2, y2 being object such that
A13: a = [x2,y2] and
A14: x2 in the carrier of (subrelstr (([#] G) \ {x})) and
y2 in the carrier of (subrelstr (([#] G) \ {x})) by RELSET_1:2;
A15: x2 in the carrier of G \ {x} by A14, YELLOW_0:def 15;
x2 = y2 by A12, A13, RELAT_1:def 10;
hence contradiction by A10, A13, A15, RELAT_1:def 10; :: thesis: verum

end;

a in [: the carrier of (subrelstr (([#] G) \ {x})), the carrier of (subrelstr (([#] G) \ {x})):] \ the InternalRel of G by A5, A9, XBOOLE_0:def 5;
hence a in the InternalRel of (ComplRelStr (subrelstr (([#] G) \ {x}))) by A6, A11, XBOOLE_0:def 5; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the InternalRel of (ComplRelStr (subrelstr (([#] G) \ {x}))) or a in the InternalRel of (subrelstr (([#] (ComplRelStr G)) \ {x9})) )
assume A16: a in the InternalRel of (ComplRelStr (subrelstr (([#] G) \ {x}))) ; :: thesis: a in the InternalRel of (subrelstr (([#] (ComplRelStr G)) \ {x9}))
then not a in id the carrier of (subrelstr (([#] G) \ {x})) by A6, XBOOLE_0:def 5;
then not a in id ( the carrier of G \ {x}) by YELLOW_0:def 15;
then A17: not a in (id the carrier of G) \ (id {x}) by SYSREL:14;

per cases ( not a in id the carrier of G or a in id {x} ) by A17, XBOOLE_0:def 5;

suppose A18: not a in id the carrier of G ; :: thesis: a in the InternalRel of (subrelstr (([#] (ComplRelStr G)) \ {x9}))

a in [: the carrier of (subrelstr (([#] G) \ {x})), the carrier of (subrelstr (([#] G) \ {x})):] \ the InternalRel of G by A6, A16, XBOOLE_0:def 5;
hence a in the InternalRel of (subrelstr (([#] (ComplRelStr G)) \ {x9})) by A5, A18, XBOOLE_0:def 5; :: thesis: verum

end;

suppose a in id {x} ; :: thesis: a in the InternalRel of (subrelstr (([#] (ComplRelStr G)) \ {x9}))

then A19: a in {[x,x]} by SYSREL:13;
thus a in the InternalRel of (subrelstr (([#] (ComplRelStr G)) \ {x9})) :: thesis: verum

proof

per cases ( a in [: the carrier of G, the carrier of G:] \ ([: the carrier of G,{x}:] \/ [:{x}, the carrier of G:]) or a in ([: the carrier of G, the carrier of G:] \ [: the carrier of G,{x}:]) /\ [:{x},{x}:] ) by A7, A6, A16, XBOOLE_0:def 3;

suppose A20: a in [: the carrier of G, the carrier of G:] \ ([: the carrier of G,{x}:] \/ [:{x}, the carrier of G:]) ; :: thesis: a in the InternalRel of (subrelstr (([#] (ComplRelStr G)) \ {x9}))

x in {x} by TARSKI:def 1;
then A21: [x,x] in [:{x}, the carrier of G:] by ZFMISC_1:87;
not a in [: the carrier of G,{x}:] \/ [:{x}, the carrier of G:] by A20, XBOOLE_0:def 5;
then not a in [:{x}, the carrier of G:] by XBOOLE_0:def 3;
hence a in the InternalRel of (subrelstr (([#] (ComplRelStr G)) \ {x9})) by A19, A21, TARSKI:def 1; :: thesis: verum

end;

suppose A22: a in ([: the carrier of G, the carrier of G:] \ [: the carrier of G,{x}:]) /\ [:{x},{x}:] ; :: thesis: a in the InternalRel of (subrelstr (([#] (ComplRelStr G)) \ {x9}))

x in {x} by TARSKI:def 1;
then A23: [x,x] in [: the carrier of G,{x}:] by ZFMISC_1:87;
a in [: the carrier of G, the carrier of G:] \ [: the carrier of G,{x}:] by A22, XBOOLE_0:def 4;
then not a in [: the carrier of G,{x}:] by XBOOLE_0:def 5;
hence a in the InternalRel of (subrelstr (([#] (ComplRelStr G)) \ {x9})) by A19, A23, TARSKI:def 1; :: thesis: verum

end;

end;

end;

end;

end;

end;

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; :: thesis: verum