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;
per cases ( [x,y] in the InternalRel of R or [x,y] in the InternalRel of R ~ ) by A2, XBOOLE_0:def 3;
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;
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;
end;