let G be non empty irreflexive RelStr ; :: thesis: for x being Element of G
for x' being Element of (ComplRelStr G) st x = x' holds
ComplRelStr (subrelstr (([#] G) \ {x})) = subrelstr (([#] (ComplRelStr G)) \ {x'})
let x be Element of G; :: thesis: for x' being Element of (ComplRelStr G) st x = x' holds
ComplRelStr (subrelstr (([#] G) \ {x})) = subrelstr (([#] (ComplRelStr G)) \ {x'})
let x' be Element of (ComplRelStr G); :: thesis: ( x = x' implies ComplRelStr (subrelstr (([#] G) \ {x})) = subrelstr (([#] (ComplRelStr G)) \ {x'}) )
assume A1: x = x' ; :: thesis: ComplRelStr (subrelstr (([#] G) \ {x})) = subrelstr (([#] (ComplRelStr G)) \ {x'})
set R = subrelstr (([#] G) \ {x});
set cR = the carrier of (subrelstr (([#] G) \ {x}));
set cG = the carrier of G;
A2: the carrier of (ComplRelStr (subrelstr (([#] G) \ {x}))) = the carrier of (subrelstr (([#] G) \ {x})) by NECKLACE:def 9
.= the carrier of G \ {x} by YELLOW_0:def 15
.= ([#] (ComplRelStr G)) \ {x'} by A1, NECKLACE:def 9
.= the carrier of (subrelstr (([#] (ComplRelStr G)) \ {x'})) by YELLOW_0:def 15 ;
A3: [#] (ComplRelStr G) = the carrier of G by NECKLACE:def 9;
A4: [:(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 ;
A5: the carrier of (subrelstr (([#] G) \ {x})) c= the carrier of G by YELLOW_0:def 13;
A6: [:the carrier of (subrelstr (([#] G) \ {x})),the carrier of (subrelstr (([#] G) \ {x})):] = [:([#] G),(([#] G) \ {x}):] \ [:{x},(([#] G) \ {x}):] by A4, ZFMISC_1:125
.= ([:([#] G),([#] G):] \ [:([#] G),{x}:]) \ [:{x},(([#] G) \ {x}):] by ZFMISC_1:125
.= ([:the carrier of G,the carrier of G:] \ [:the carrier of G,{x}:]) \ ([:{x},the carrier of G:] \ [:{x},{x}:]) by ZFMISC_1:125
.= (([: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 ;
A7: the InternalRel of (ComplRelStr (subrelstr (([#] G) \ {x}))) = (the InternalRel of (subrelstr (([#] G) \ {x})) ` ) \ (id the carrier of (subrelstr (([#] G) \ {x}))) by NECKLACE:def 9
.= ([: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 5
.= ([: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}))) ;
A8: the InternalRel of (subrelstr (([#] (ComplRelStr G)) \ {x'})) = the InternalRel of (ComplRelStr G) |_2 the carrier of (subrelstr (([#] (ComplRelStr G)) \ {x'})) by YELLOW_0:def 14
.= the InternalRel of (ComplRelStr G) |_2 (the carrier of G \ {x}) by A1, A3, 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 9
.= ([: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: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 5
.= (([: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 A5, XBOOLE_1:28, ZFMISC_1:119 ;
the InternalRel of (subrelstr (([#] (ComplRelStr G)) \ {x'})) = the InternalRel of (ComplRelStr (subrelstr (([#] G) \ {x})))

proof

thus the InternalRel of (subrelstr (([#] (ComplRelStr G)) \ {x'})) 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)) \ {x'}))

proof

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

proof

assume A10: a in id the carrier of (subrelstr (([#] G) \ {x})) ; :: thesis: contradiction
then consider x2, y2 being set such that
A11: ( a = [x2,y2] & x2 in the carrier of (subrelstr (([#] G) \ {x})) & y2 in the carrier of (subrelstr (([#] G) \ {x})) ) by RELSET_1:6;
A12: ( x2 in the carrier of G \ {x} & y2 in the carrier of G \ {x} ) by A11, YELLOW_0:def 15;
x2 = y2 by A10, A11, RELAT_1:def 10;
hence contradiction by A9, A11, A12, RELAT_1:def 10; :: thesis: verum

end;

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

end;

let a be set ; :: 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)) \ {x'})) )
assume A13: a in the InternalRel of (ComplRelStr (subrelstr (([#] G) \ {x}))) ; :: thesis: a in the InternalRel of (subrelstr (([#] (ComplRelStr G)) \ {x'}))
then ( a in [:the carrier of (subrelstr (([#] G) \ {x})),the carrier of (subrelstr (([#] G) \ {x})):] \ the InternalRel of G & not a in id the carrier of (subrelstr (([#] G) \ {x})) ) by A7, XBOOLE_0:def 5;
then not a in id (the carrier of G \ {x}) by YELLOW_0:def 15;
then A14: not a in (id the carrier of G) \ (id {x}) by SYSREL:32;

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

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

then ( a in [:the carrier of (subrelstr (([#] G) \ {x})),the carrier of (subrelstr (([#] G) \ {x})):] \ the InternalRel of G & not a in id the carrier of G ) by A7, A13, XBOOLE_0:def 5;
hence a in the InternalRel of (subrelstr (([#] (ComplRelStr G)) \ {x'})) by A8, XBOOLE_0:def 5; :: thesis: verum

end;

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

then A15: a in {[x,x]} by SYSREL:30;
thus a in the InternalRel of (subrelstr (([#] (ComplRelStr G)) \ {x'})) :: 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 A6, A7, A13, XBOOLE_0:def 3;

suppose 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)) \ {x'}))

then ( a in [:the carrier of G,the carrier of G:] & not a in [:the carrier of G,{x}:] \/ [:{x},the carrier of G:] ) by XBOOLE_0:def 5;
then A16: ( a in [:the carrier of G,the carrier of G:] & not a in [:the carrier of G,{x}:] & not a in [:{x},the carrier of G:] ) by XBOOLE_0:def 3;
( x in {x} & x in the carrier of G ) by TARSKI:def 1;
then [x,x] in [:{x},the carrier of G:] by ZFMISC_1:106;
hence a in the InternalRel of (subrelstr (([#] (ComplRelStr G)) \ {x'})) by A15, A16, TARSKI:def 1; :: thesis: verum

end;

suppose 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)) \ {x'}))

then a in [:the carrier of G,the carrier of G:] \ [:the carrier of G,{x}:] by XBOOLE_0:def 4;
then A17: ( a in [:the carrier of G,the carrier of G:] & not a in [:the carrier of G,{x}:] ) by XBOOLE_0:def 5;
( x in {x} & x in the carrier of G ) by TARSKI:def 1;
then [x,x] in [:the carrier of G,{x}:] by ZFMISC_1:106;
hence a in the InternalRel of (subrelstr (([#] (ComplRelStr G)) \ {x'})) by A15, A17, TARSKI:def 1; :: thesis: verum

end;

end;

end;

end;

end;

end;

hence ComplRelStr (subrelstr (([#] G) \ {x})) = subrelstr (([#] (ComplRelStr G)) \ {x'}) by A2; :: thesis: verum