let G be _Graph; :: thesis: for S being Subset of ()
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 (); :: 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 () 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 ;
then A4: e in the_Edges_of H by GLIB_000:def 37;
the_Target_of H = () | () by GLIB_000:45;
then A5: (the_Target_of H) . e = () . e by ;
A6: ( ( (the_Source_of G) . e = u & () . e = v ) or ( () . e = v & () . e = u ) ) by A3;
the_Source_of H = () | () by GLIB_000:45;
then (the_Source_of H) . e = () . e by ;
hence e Joins u,v,H by A4, A6, A5; :: thesis: verum