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})))

.= 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

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

the carrier of (ComplRelStr (subrelstr (([#] G) \ {x}))) =
the carrier of (subrelstr (([#] G) \ {x}))
by NECKLACE:def 8
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}))

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;

end;proof

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})) )
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}))

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

end;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

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;
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;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

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

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;

end;

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;hence a in the InternalRel of (subrelstr (([#] (ComplRelStr G)) \ {x9})) by A5, A18, XBOOLE_0:def 5; :: thesis: verum

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

end;thus a in the InternalRel of (subrelstr (([#] (ComplRelStr G)) \ {x9})) :: thesis: verum

proof
end;

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;

end;

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;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

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;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

.= 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