let G1 be _Graph; :: thesis: for G2 being inducedSubgraph of G1,(the_Vertices_of G1) holds G1 == G2
let G2 be inducedSubgraph of G1,(the_Vertices_of G1); :: thesis: G1 == G2
the_Vertices_of G1 c= the_Vertices_of G1 ;
then A1: ( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = G1 .edgesBetween (the_Vertices_of G1) ) by Def39;
then A2: the_Edges_of G2 = the_Edges_of G1 by Th37;
then ( the_Source_of G2 = (the_Source_of G1) | (the_Edges_of G1) & the_Target_of G2 = (the_Target_of G1) | (the_Edges_of G1) ) by Th48;
then ( the_Source_of G2 = (the_Source_of G1) | (dom (the_Source_of G1)) & the_Target_of G2 = (the_Target_of G1) | (dom (the_Target_of G1)) ) by FUNCT_2:def 1;
then ( the_Source_of G2 = the_Source_of G1 & the_Target_of G2 = the_Target_of G1 ) by RELAT_1:98;
hence G1 == G2 by A1, A2, Def36; :: thesis: verum