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

suppose n is zero ; :: thesis: for b₁ being total Relation of (n -tuples_on X) st b₁ = n -placesOf R holds
b₁ is transitive

hence for b₁ being total Relation of (n -tuples_on X) st b₁ = n -placesOf R holds
b₁ is transitive by Lm8; :: thesis: verum

end;

suppose not n is zero ; :: thesis: for b₁ being total Relation of (n -tuples_on X) st b₁ = n -placesOf R holds
b₁ is transitive

hence for b₁ being total Relation of (n -tuples_on X) st b₁ = n -placesOf R holds
b₁ is transitive by Lm7; :: thesis: verum

end;

end;