id V is isometric by Th5;
hence not ISOM V is empty by Def4; :: thesis: verum