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 )
A1: field R = X by ORDERS_1:97;
assume [x,y] in R ; :: thesis: [y,x] in R
then A2: ( x in X & y in X & [x,y] in R ) by Lm1;
R is_symmetric_in X by A1, RELAT_2:def 11;
hence [y,x] in R by A2, RELAT_2:def 3; :: thesis: verum