let X, x, y be set ; :: thesis: for R being symmetric total Relation of X st [x,y] in R holds
[y,x] in R
let R be symmetric total Relation of X; :: thesis: ( [x,y] in R implies [y,x] in R )
field R = X by ORDERS_1:12;
then A1: R is_symmetric_in X by RELAT_2:def 11;
assume A2: [x,y] in R ; :: thesis: [y,x] in R
then ( x in X & y in X ) by Lm1;
hence [y,x] in R by A2, A1, RELAT_2:def 3; :: thesis: verum