let x, y be object ; :: according to NECKLACE:def 3,RELAT_2: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 () )
set S = ComplRelStr R;
assume that
A1: ( x in the carrier of () & y in the carrier of () ) and
A2: [x,y] in the InternalRel of () ; :: thesis: [y,x] in the InternalRel of ()
per cases ( x = y or x <> y ) ;
suppose x = y ; :: thesis: [y,x] in the InternalRel of ()
hence [y,x] in the InternalRel of () by A2; :: thesis: verum
end;
suppose A3: x <> y ; :: thesis: [y,x] in the InternalRel of ()
A4: ( x in the carrier of R & y in the carrier of R ) by ;
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 ;
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 ;
then A7: [y,x] in the InternalRel of R ` by SUBSET_1:def 4;
not [y,x] in id the carrier of R by ;
then [y,x] in ( the InternalRel of R `) \ (id the carrier of R) by ;
hence [y,x] in the InternalRel of () by NECKLACE:def 8; :: thesis: verum
end;
end;