hereby :: thesis: ( ( not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) implies ex b₁ being Subgraph of G st b₁ == G )

assume that
A1: V is non empty Subset of (the_Vertices_of G) and
A2: E c= G .edgesBetween V ; :: thesis: ex IT being Subgraph of G st
( the_Vertices_of IT = V & the_Edges_of IT = E )
reconsider E9 = E as Subset of (the_Edges_of G) by A2, XBOOLE_1:1;
set S = (the_Source_of G) | E9;
set T = (the_Target_of G) | E9;
reconsider V9 = V as non empty Subset of (the_Vertices_of G) by A1;
dom (the_Target_of G) = the_Edges_of G by FUNCT_2:def 1;
then A3: dom ((the_Target_of G) | E9) = E9 by RELAT_1:62;

now :: thesis: for e being object st e in E9 holds
((the_Target_of G) | E9) . e in V

let e be object ; :: thesis: ( e in E9 implies ((the_Target_of G) | E9) . e in V )
assume A4: e in E9 ; :: thesis: ((the_Target_of G) | E9) . e in V
then e in G .edgesInto V by A2, XBOOLE_0:def 4;
then (the_Target_of G) . e in V by Def26;
hence ((the_Target_of G) | E9) . e in V by A4, FUNCT_1:49; :: thesis: verum

end;

then reconsider T = (the_Target_of G) | E9 as Function of E9,V9 by A3, FUNCT_2:3;
dom (the_Source_of G) = the_Edges_of G by FUNCT_2:def 1;
then A5: dom ((the_Source_of G) | E9) = E9 by RELAT_1:62;

now :: thesis: for e being object st e in E9 holds
((the_Source_of G) | E9) . e in V

let e be object ; :: thesis: ( e in E9 implies ((the_Source_of G) | E9) . e in V )
assume A6: e in E9 ; :: thesis: ((the_Source_of G) | E9) . e in V
then e in G .edgesOutOf V by A2, XBOOLE_0:def 4;
then (the_Source_of G) . e in V by Def27;
hence ((the_Source_of G) | E9) . e in V by A6, FUNCT_1:49; :: thesis: verum

end;

then reconsider S = (the_Source_of G) | E9 as Function of E9,V9 by A5, FUNCT_2:3;
set IT = createGraph (V9,E9,S,T);
( the_Vertices_of (createGraph (V9,E9,S,T)) = V & ( for e being set st e in the_Edges_of (createGraph (V9,E9,S,T)) holds
( (the_Source_of (createGraph (V9,E9,S,T))) . e = (the_Source_of G) . e & (the_Target_of (createGraph (V9,E9,S,T))) . e = (the_Target_of G) . e ) ) ) by FUNCT_1:49;
then reconsider IT = createGraph (V9,E9,S,T) as Subgraph of G by Def32;
take IT = IT; :: thesis: ( the_Vertices_of IT = V & the_Edges_of IT = E )
thus ( the_Vertices_of IT = V & the_Edges_of IT = E ) ; :: thesis: verum

end;

G is Subgraph of G by Lm3;
hence ( ( not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) implies ex b₁ being Subgraph of G st b₁ == G ) ; :: thesis: verum