( id V is onto & id V is isometric ) ;
hence not ISOM V is empty by Def4; :: thesis: verum