inversions R c= [:(dom R),(dom R):] by TW1;
hence inversions R is finite ; :: thesis: verum