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