( firstdom {} = {} & lastrng {} = {} ) by Def5, Def6;