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

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