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

end;

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

b_{1} is transitive

b

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

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

end;b

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

b_{1} is transitive

b

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

b_{1} is transitive
by Lm7; :: thesis: verum

end;b