let V1 be non empty set ; :: thesis: for V2 being non empty Subset of V1
for E1 being Relation of V1
for E2 being Relation of V2 st E2 c= E1 holds
createGraph (V2,E2) is inducedSubgraph of createGraph (V1,E1),V2,E2
let V2 be non empty Subset of V1; :: thesis: for E1 being Relation of V1
for E2 being Relation of V2 st E2 c= E1 holds
createGraph (V2,E2) is inducedSubgraph of createGraph (V1,E1),V2,E2
let E1 be Relation of V1; :: thesis: for E2 being Relation of V2 st E2 c= E1 holds
createGraph (V2,E2) is inducedSubgraph of createGraph (V1,E1),V2,E2
let E2 be Relation of V2; :: thesis: ( E2 c= E1 implies createGraph (V2,E2) is inducedSubgraph of createGraph (V1,E1),V2,E2 )
assume A1: E2 c= E1 ; :: thesis: createGraph (V2,E2) is inducedSubgraph of createGraph (V1,E1),V2,E2
set G1 = createGraph (V1,E1);
set G2 = createGraph (V2,E2);
A2: ( the_Vertices_of (createGraph (V2,E2)) = V2 & the_Edges_of (createGraph (V2,E2)) = E2 ) ;
A3: V2 is non empty Subset of (the_Vertices_of (createGraph (V1,E1))) ;
then A7: E2 c= (createGraph (V1,E1)) .edgesBetween V2 by TARSKI:def 3;
createGraph (V2,E2) is Subgraph of createGraph (V1,E1) hence createGraph (V2,E2) is inducedSubgraph of createGraph (V1,E1),V2,E2 by A2, A3, A7, GLIB_000:def 37; :: thesis: verum