let x, y be object ; :: according to RELAT_2:def 3,NECKLACE:def 3 :: thesis: ( not x in the carrier of (SymRelStr R) or not y in the carrier of (SymRelStr R) or not [x,y] in the InternalRel of (SymRelStr R) or [y,x] in the InternalRel of (SymRelStr R) )

assume that

x in the carrier of (SymRelStr R) and

y in the carrier of (SymRelStr R) and

A1: [x,y] in the InternalRel of (SymRelStr R) ; :: thesis: [y,x] in the InternalRel of (SymRelStr R)

A2: [x,y] in the InternalRel of R \/ ( the InternalRel of R ~) by A1, Def7;

assume that

x in the carrier of (SymRelStr R) and

y in the carrier of (SymRelStr R) and

A1: [x,y] in the InternalRel of (SymRelStr R) ; :: thesis: [y,x] in the InternalRel of (SymRelStr R)

A2: [x,y] in the InternalRel of R \/ ( the InternalRel of R ~) by A1, Def7;

per cases
( [x,y] in the InternalRel of R or [x,y] in the InternalRel of R ~ )
by A2, XBOOLE_0:def 3;

end;

suppose
[x,y] in the InternalRel of R
; :: thesis: [y,x] in the InternalRel of (SymRelStr R)

then
[y,x] in the InternalRel of R ~
by RELAT_1:def 7;

then [y,x] in the InternalRel of R \/ ( the InternalRel of R ~) by XBOOLE_0:def 3;

hence [y,x] in the InternalRel of (SymRelStr R) by Def7; :: thesis: verum

end;then [y,x] in the InternalRel of R \/ ( the InternalRel of R ~) by XBOOLE_0:def 3;

hence [y,x] in the InternalRel of (SymRelStr R) by Def7; :: thesis: verum

suppose
[x,y] in the InternalRel of R ~
; :: thesis: [y,x] in the InternalRel of (SymRelStr R)

then
[y,x] in the InternalRel of R
by RELAT_1:def 7;

then [y,x] in the InternalRel of R \/ ( the InternalRel of R ~) by XBOOLE_0:def 3;

hence [y,x] in the InternalRel of (SymRelStr R) by Def7; :: thesis: verum

end;then [y,x] in the InternalRel of R \/ ( the InternalRel of R ~) by XBOOLE_0:def 3;

hence [y,x] in the InternalRel of (SymRelStr R) by Def7; :: thesis: verum