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)

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

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