let x, y be object ; :: according to RELAT_2:def 3,NECKLACE:def 3 :: thesis: ( not x in the carrier of () or not y in the carrier of () or not [x,y] in the InternalRel of () or [y,x] in the InternalRel of () )
assume that
x in the carrier of () and
y in the carrier of () and
A1: [x,y] in the InternalRel of () ; :: thesis: [y,x] in the InternalRel of ()
A2: [x,y] in the InternalRel of R \/ ( the InternalRel of R ~) by ;
per cases ( [x,y] in the InternalRel of R or [x,y] in the InternalRel of R ~ ) by ;
suppose [x,y] in the InternalRel of R ; :: thesis: [y,x] in the InternalRel of ()
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 () by Def7; :: thesis: verum
end;
suppose [x,y] in the InternalRel of R ~ ; :: thesis: [y,x] in the InternalRel of ()
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 () by Def7; :: thesis: verum
end;
end;