let G be _Graph; :: thesis: for S being Subset of (the_Vertices_of G)
for H being inducedSubgraph of G,S
for u, v being object st u in S & v in S holds
for e being object st e Joins u,v,G holds
e Joins u,v,H
let S be Subset of (the_Vertices_of G); :: thesis: for H being inducedSubgraph of G,S
for u, v being object st u in S & v in S holds
for e being object st e Joins u,v,G holds
e Joins u,v,H
let H be inducedSubgraph of G,S; :: thesis: for u, v being object st u in S & v in S holds
for e being object st e Joins u,v,G holds
e Joins u,v,H
let u, v be object ; :: thesis: ( u in S & v in S implies for e being object st e Joins u,v,G holds
e Joins u,v,H )
assume that
A1: u in S and
A2: v in S ; :: thesis: for e being object st e Joins u,v,G holds
e Joins u,v,H
reconsider S = S as non empty Subset of (the_Vertices_of G) by A1;
let e be object ; :: thesis: ( e Joins u,v,G implies e Joins u,v,H )
assume A3: e Joins u,v,G ; :: thesis: e Joins u,v,H
e in G .edgesBetween S by A1, A2, A3, GLIB_000:32;
then A4: e in the_Edges_of H by GLIB_000:def 37;
the_Target_of H = (the_Target_of G) | (the_Edges_of H) by GLIB_000:45;
then A5: (the_Target_of H) . e = (the_Target_of G) . e by A4, FUNCT_1:49;
A6: ( ( (the_Source_of G) . e = u & (the_Target_of G) . e = v ) or ( (the_Source_of G) . e = v & (the_Target_of G) . e = u ) ) by A3;
the_Source_of H = (the_Source_of G) | (the_Edges_of H) by GLIB_000:45;
then (the_Source_of H) . e = (the_Source_of G) . e by A4, FUNCT_1:49;
hence e Joins u,v,H by A4, A6, A5; :: thesis: verum