x * (x \ y) = y ;
hence y / (x \ y) = x ; :: thesis: verum