let x, y be object ; :: according to NECKLACE:def 3,RELAT_2:def 3 :: thesis: ( not x in the carrier of (ComplRelStr R) or not y in the carrier of (ComplRelStr R) or not [x,y] in the InternalRel of (ComplRelStr R) or [y,x] in the InternalRel of (ComplRelStr R) )
set S = ComplRelStr R;
assume that
A1: ( x in the carrier of (ComplRelStr R) & y in the carrier of (ComplRelStr R) ) and
A2: [x,y] in the InternalRel of (ComplRelStr R) ; :: thesis: [y,x] in the InternalRel of (ComplRelStr R)

per cases ( x = y or x <> y ) ;

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

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

end;

suppose A3: x <> y ; :: thesis: [y,x] in the InternalRel of (ComplRelStr R)

A4: ( x in the carrier of R & y in the carrier of R ) by A1, NECKLACE:def 8;
then A5: [y,x] in [: the carrier of R, the carrier of R:] by ZFMISC_1:87;
[x,y] in ( the InternalRel of R `) \ (id the carrier of R) by A2, NECKLACE:def 8;
then [x,y] in the InternalRel of R ` by XBOOLE_0:def 5;
then [x,y] in [: the carrier of R, the carrier of R:] \ the InternalRel of R by SUBSET_1:def 4;
then A6: not [x,y] in the InternalRel of R by XBOOLE_0:def 5;
the InternalRel of R is_symmetric_in the carrier of R by NECKLACE:def 3;
then not [y,x] in the InternalRel of R by A4, A6;
then [y,x] in [: the carrier of R, the carrier of R:] \ the InternalRel of R by A5, XBOOLE_0:def 5;
then A7: [y,x] in the InternalRel of R ` by SUBSET_1:def 4;
not [y,x] in id the carrier of R by A3, RELAT_1:def 10;
then [y,x] in ( the InternalRel of R `) \ (id the carrier of R) by A7, XBOOLE_0:def 5;
hence [y,x] in the InternalRel of (ComplRelStr R) by NECKLACE:def 8; :: thesis: verum

end;

end;