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