let R be Relation; :: thesis: ( R is symmetric iff for x, y being object st [x,y] in R holds
[y,x] in R )
thus ( R is symmetric implies for x, y being object st [x,y] in R holds
[y,x] in R ) :: thesis: ( ( for x, y being object st [x,y] in R holds
[y,x] in R ) implies R is symmetric )
proof
assume A0: R is symmetric ; :: thesis: for x, y being object st [x,y] in R holds
[y,x] in R
let x, y be object ; :: thesis: ( [x,y] in R implies [y,x] in R )
assume A1: [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 A0, A1, RELAT_2:def 3, RELAT_2:def 11; :: thesis: verum
end;
assume A1: for x, y being object st [x,y] in R holds
[y,x] in R ; :: thesis: R is symmetric
set X = field R;
for x, y being object st x in field R & y in field R & [x,y] in R holds
[y,x] in R by A1;
hence R is symmetric by RELAT_2:def 11, RELAT_2:def 3; :: thesis: verum