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
A1: the_Vertices_of G1 c= the_Vertices_of G1 ;
then the_Edges_of G2 = G1 .edgesBetween (the_Vertices_of G1) by Def37;
then A2: the_Edges_of G2 = the_Edges_of G1 by Th34;
then the_Source_of G2 = (the_Source_of G1) | (the_Edges_of G1) by Th45;
then the_Source_of G2 = (the_Source_of G1) | (dom (the_Source_of G1)) ;
then A3: the_Source_of G2 = the_Source_of G1 ;
the_Target_of G2 = (the_Target_of G1) | (the_Edges_of G1) by A2, Th45;
then the_Target_of G2 = (the_Target_of G1) | (dom (the_Target_of G1)) ;
then A4: the_Target_of G2 = the_Target_of G1 ;
the_Vertices_of G2 = the_Vertices_of G1 by A1, Def37;
hence G1 == G2 by A2, A3, A4; :: thesis: verum