let x, y be object ; :: according to RELAT_2:def 3,RELAT_2:def 11 :: thesis: ( not x in field the InternalRel of R or not y in field the InternalRel of R or not [x,y] in the InternalRel of R or [y,x] in the InternalRel of R )
assume A1: ( x in field the InternalRel of R & y in field the InternalRel of R & [x,y] in the InternalRel of R ) ; :: thesis: [y,x] in the InternalRel of R
( the InternalRel of R is_symmetric_in the carrier of R & field the InternalRel of R c= the carrier of R \/ the carrier of R ) by Def3, RELSET_1:8;
hence [y,x] in the InternalRel of R by A1; :: thesis: verum