let x, y be object ; :: thesis: for R being Relation st R is symmetric & [x,y] in R holds
[y,x] in R
let R be Relation; :: thesis: ( R is symmetric & [x,y] in R implies [y,x] in R )
assume A1: R is symmetric ; :: thesis: ( not [x,y] in R or [y,x] in R )
assume A2: [x,y] in R ; :: thesis: [y,x] in R
then ( x in field R & y in field R ) by RELAT_1:15;
hence [y,x] in R by A1, RELAT_2:def 11, RELAT_2:def 3, A2; :: thesis: verum