let X be set ; :: thesis: for x, y being object

for R being symmetric total Relation of X holds

( y in Class (R,x) iff [y,x] in R )

let x, y be object ; :: 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) )

then A1: [x,y] in R by Th6;

x in {x} by TARSKI:def 1;

hence y in Class (R,x) by A1, RELAT_1:def 13; :: thesis: verum

for R being symmetric total Relation of X holds

( y in Class (R,x) iff [y,x] in R )

let x, y be object ; :: 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,x] in R
; :: thesis: y in Class (R,x)
assume
y in Class (R,x)
; :: thesis: [y,x] in R

then ex z being object 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 Th6; :: thesis: verum

end;then ex z being object 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 Th6; :: thesis: verum

then A1: [x,y] in R by Th6;

x in {x} by TARSKI:def 1;

hence y in Class (R,x) by A1, RELAT_1:def 13; :: thesis: verum