per cases ( n is zero or not n is zero ) ;
suppose n is zero ; :: thesis: for b1 being total Relation of (n -tuples_on X) st b1 = n -placesOf R holds
b1 is transitive
hence for b1 being total Relation of (n -tuples_on X) st b1 = n -placesOf R holds
b1 is transitive by Lm8; :: thesis: verum
end;
suppose not n is zero ; :: thesis: for b1 being total Relation of (n -tuples_on X) st b1 = n -placesOf R holds
b1 is transitive
hence for b1 being total Relation of (n -tuples_on X) st b1 = n -placesOf R holds
b1 is transitive by Lm7; :: thesis: verum
end;
end;