reconsider E = {} as finite Subset of (G .edgesBetween {v}) by XBOOLE_1:2;
let IT be inducedSubgraph of G,{v}, {} ; :: thesis: ( IT is _finite & IT is _trivial )
IT is inducedSubgraph of G,{v},E ;
hence ( IT is _finite & IT is _trivial ) ; :: thesis: verum