let G be _Graph; :: thesis: for V1, V2, E1, E2 being set
for G1 being inducedSubgraph of G,V1,E1
for G2 being inducedSubgraph of G,V2,E2 st V2 c= V1 & E2 c= E1 & V2 is non empty Subset of (the_Vertices_of G) & E2 c= G .edgesBetween V2 holds
G2 is Subgraph of G1
let V1, V2, E1, E2 be set ; :: thesis: for G1 being inducedSubgraph of G,V1,E1
for G2 being inducedSubgraph of G,V2,E2 st V2 c= V1 & E2 c= E1 & V2 is non empty Subset of (the_Vertices_of G) & E2 c= G .edgesBetween V2 holds
G2 is Subgraph of G1
let G1 be inducedSubgraph of G,V1,E1; :: thesis: for G2 being inducedSubgraph of G,V2,E2 st V2 c= V1 & E2 c= E1 & V2 is non empty Subset of (the_Vertices_of G) & E2 c= G .edgesBetween V2 holds
G2 is Subgraph of G1
let G2 be inducedSubgraph of G,V2,E2; :: thesis: ( V2 c= V1 & E2 c= E1 & V2 is non empty Subset of (the_Vertices_of G) & E2 c= G .edgesBetween V2 implies G2 is Subgraph of G1 )
assume that
A1: ( V2 c= V1 & E2 c= E1 ) and
A2: ( V2 is non empty Subset of (the_Vertices_of G) & E2 c= G .edgesBetween V2 ) ; :: thesis: G2 is Subgraph of G1
A3: ( the_Vertices_of G2 = V2 & the_Edges_of G2 = E2 ) by A2, Def37;

now :: thesis: G2 is Subgraph of G1

per cases ( ( V1 is non empty Subset of (the_Vertices_of G) & E1 c= G .edgesBetween V1 ) or not V1 is non empty Subset of (the_Vertices_of G) or not E1 c= G .edgesBetween V1 ) ;

suppose ( V1 is non empty Subset of (the_Vertices_of G) & E1 c= G .edgesBetween V1 ) ; :: thesis: G2 is Subgraph of G1

then ( the_Vertices_of G1 = V1 & the_Edges_of G1 = E1 ) by Def37;
hence G2 is Subgraph of G1 by A1, A3, Th44; :: thesis: verum

end;

suppose ( not V1 is non empty Subset of (the_Vertices_of G) or not E1 c= G .edgesBetween V1 ) ; :: thesis: G2 is Subgraph of G1

then G1 == G by Def37;
hence G2 is Subgraph of G1 by A3, Th44; :: thesis: verum

end;

end;

end;

hence G2 is Subgraph of G1 ; :: thesis: verum