let G be non empty irreflexive RelStr ; :: thesis: for x being Element of
for x' being Element of st x = x' holds
ComplRelStr (subrelstr (([#] G) \ {x})) = subrelstr (([#] (ComplRelStr G)) \ {x'})
let x be Element of ; :: thesis: for x' being Element of st x = x' holds
ComplRelStr (subrelstr (([#] G) \ {x})) = subrelstr (([#] (ComplRelStr G)) \ {x'})
let x' be Element of ; :: 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: [#] (ComplRelStr G) = the carrier of G by NECKLACE:def 9;
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)) \ {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, 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 9
.= ([: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 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 A4, XBOOLE_1:28, ZFMISC_1:119 ;
A6: 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}))) ;
A7: [:the carrier of (subrelstr (([#] G) \ {x})),the carrier of (subrelstr (([#] G) \ {x})):] = [:([#] G),(([#] G) \ {x}):] \ [:{x},(([#] G) \ {x}):] by A3, 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 ;
A8: 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 A9: a in the InternalRel of (subrelstr (([#] (ComplRelStr G)) \ {x'})) ; :: 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 set 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:6;
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 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 A16: a in the InternalRel of (ComplRelStr (subrelstr (([#] G) \ {x}))) ; :: thesis: a in the InternalRel of (subrelstr (([#] (ComplRelStr G)) \ {x'}))
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:32;

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

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)) \ {x'})) by A5, A18, XBOOLE_0:def 5; :: thesis: verum

end;

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

then A19: 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 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)) \ {x'}))

x in {x} by TARSKI:def 1;
then A21: [x,x] in [:{x},the carrier of G:] by ZFMISC_1:106;
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)) \ {x'})) 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)) \ {x'}))

x in {x} by TARSKI:def 1;
then A23: [x,x] in [:the carrier of G,{x}:] by ZFMISC_1:106;
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)) \ {x'})) 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 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 ;
hence ComplRelStr (subrelstr (([#] G) \ {x})) = subrelstr (([#] (ComplRelStr G)) \ {x'}) by A8; :: thesis: verum