reconsider E = {} as Subset of (G .edgesBetween V) by XBOOLE_1:2;
let IT be inducedSubgraph of G,V, {} ; :: thesis: IT is simple
IT is inducedSubgraph of G,V,E ;
then ( the_Vertices_of IT = V & the_Edges_of IT = {} ) by Def39;
hence IT is simple by Lm3; :: thesis: verum