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

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

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

end;

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

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

end;

end;