let G be non empty irreflexive RelStr ; :: thesis: for x being Element of G
for x9 being Element of () st x = x9 holds
ComplRelStr (subrelstr (([#] G) \ {x})) = subrelstr (([#] ()) \ {x9})

let x be Element of G; :: thesis: for x9 being Element of () st x = x9 holds
ComplRelStr (subrelstr (([#] G) \ {x})) = subrelstr (([#] ()) \ {x9})

let x9 be Element of (); :: thesis: ( x = x9 implies ComplRelStr (subrelstr (([#] G) \ {x})) = subrelstr (([#] ()) \ {x9}) )
assume A1: x = x9 ; :: thesis: ComplRelStr (subrelstr (([#] G) \ {x})) = subrelstr (([#] ()) \ {x9})
set R = subrelstr (([#] G) \ {x});
set cR = the carrier of (subrelstr (([#] G) \ {x}));
set cG = the carrier of G;
A2: [#] () = 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 (([#] ()) \ {x9})) = the InternalRel of () |_2 the carrier of (subrelstr (([#] ()) \ {x9})) by YELLOW_0:def 14
.= the InternalRel of () |_2 ( the carrier of G \ {x}) by
.= (( 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
.= ([: 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 ;
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
.= ([:([#] 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 (([#] ()) \ {x9})) = the InternalRel of (ComplRelStr (subrelstr (([#] G) \ {x})))
proof
thus the InternalRel of (subrelstr (([#] ()) \ {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 (([#] ()) \ {x9}))
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the InternalRel of (subrelstr (([#] ()) \ {x9})) or a in the InternalRel of (ComplRelStr (subrelstr (([#] G) \ {x}))) )
assume A9: a in the InternalRel of (subrelstr (([#] ()) \ {x9})) ; :: thesis: a in the InternalRel of (ComplRelStr (subrelstr (([#] G) \ {x})))
then A10: not a in id the carrier of G by ;
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 ;
x2 = y2 by ;
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 ;
hence a in the InternalRel of (ComplRelStr (subrelstr (([#] G) \ {x}))) by ; :: 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 (([#] ()) \ {x9})) )
assume A16: a in the InternalRel of (ComplRelStr (subrelstr (([#] G) \ {x}))) ; :: thesis: a in the InternalRel of (subrelstr (([#] ()) \ {x9}))
then not a in id the carrier of (subrelstr (([#] G) \ {x})) by ;
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 ;
suppose A18: not a in id the carrier of G ; :: thesis: a in the InternalRel of (subrelstr (([#] ()) \ {x9}))
a in [: the carrier of (subrelstr (([#] G) \ {x})), the carrier of (subrelstr (([#] G) \ {x})):] \ the InternalRel of G by ;
hence a in the InternalRel of (subrelstr (([#] ()) \ {x9})) by ; :: thesis: verum
end;
suppose a in id {x} ; :: thesis: a in the InternalRel of (subrelstr (([#] ()) \ {x9}))
then A19: a in {[x,x]} by SYSREL:13;
thus a in the InternalRel of (subrelstr (([#] ()) \ {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 ;
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 (([#] ()) \ {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 ;
then not a in [:{x}, the carrier of G:] by XBOOLE_0:def 3;
hence a in the InternalRel of (subrelstr (([#] ()) \ {x9})) by ; :: 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 (([#] ()) \ {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 ;
then not a in [: the carrier of G,{x}:] by XBOOLE_0:def 5;
hence a in the InternalRel of (subrelstr (([#] ()) \ {x9})) by ; :: 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
.= ([#] ()) \ {x9} by
.= the carrier of (subrelstr (([#] ()) \ {x9})) by YELLOW_0:def 15 ;
hence ComplRelStr (subrelstr (([#] G) \ {x})) = subrelstr (([#] ()) \ {x9}) by A8; :: thesis: verum