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