let R be Relation; ( 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 )
( ( 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
;
for x, y being object st [x,y] in R holds
[y,x] in R
let x,
y be
object ;
( [x,y] in R implies [y,x] in R )
assume A1:
[x,y] in R
;
[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;
verum
end;
assume A1:
for x, y being object st [x,y] in R holds
[y,x] in R
; 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; verum