let x, y be set ; :: 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 that
A1: ( x in field the InternalRel of R & y in field the InternalRel of R ) and
A2: [x,y] in the InternalRel of R ; :: thesis: [y,x] in the InternalRel of R
A3: the InternalRel of R is_symmetric_in the carrier of R by Def4;
field the InternalRel of R c= the carrier of R \/ the carrier of R by RELSET_1:19;
hence [y,x] in the InternalRel of R by A1, A2, A3, RELAT_2:def 3; :: thesis: verum