let X, y, x be set ; :: thesis: for R being symmetric total Relation of X holds
( y in Class R,x iff [y,x] in R )
let R be symmetric total Relation of X; :: thesis: ( y in Class R,x iff [y,x] in R )
thus ( y in Class R,x implies [y,x] in R ) :: thesis: ( [y,x] in R implies y in Class R,x )

proof

assume y in Class R,x ; :: thesis: [y,x] in R
then ex z being set st
( [z,y] in R & z in {x} ) by RELAT_1:def 13;
then [x,y] in R by TARSKI:def 1;
hence [y,x] in R by Th12; :: thesis: verum

end;

assume [y,x] in R ; :: thesis: y in Class R,x
then A1: [x,y] in R by Th12;
x in {x} by TARSKI:def 1;
hence y in Class R,x by A1, RELAT_1:def 13; :: thesis: verum