per cases
( n is zero or not n is zero )
;

end;

suppose
n is zero
; :: thesis: for b_{1} being Relation of (n -tuples_on X) st b_{1} = n -placesOf R holds

b_{1} is symmetric

b

hence
for b_{1} being Relation of (n -tuples_on X) st b_{1} = n -placesOf R holds

b_{1} is symmetric
by Lm8; :: thesis: verum

end;b

suppose
not n is zero
; :: thesis: for b_{1} being Relation of (n -tuples_on X) st b_{1} = n -placesOf R holds

b_{1} is symmetric

b

hence
for b_{1} being Relation of (n -tuples_on X) st b_{1} = n -placesOf R holds

b_{1} is symmetric
by Lm6; :: thesis: verum

end;b