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 A1: ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V ) ; :: thesis: ex IT being Subgraph of G st
( the_Vertices_of IT = V & the_Edges_of IT = E )
then reconsider V' = V as non empty Subset of (the_Vertices_of G) ;
reconsider E' = E as Subset of (the_Edges_of G) by A1, XBOOLE_1:1;
set S = (the_Source_of G) | E';
set T = (the_Target_of G) | E';
( dom (the_Source_of G) = the_Edges_of G & dom (the_Target_of G) = the_Edges_of G ) by FUNCT_2:def 1;
then A2: ( dom ((the_Source_of G) | E') = E' & dom ((the_Target_of G) | E') = E' ) by RELAT_1:91;

now

let e be set ; :: thesis: ( e in E' implies ((the_Source_of G) | E') . e in V )
assume A3: e in E' ; :: thesis: ((the_Source_of G) | E') . e in V
then e in G .edgesOutOf V by A1, XBOOLE_0:def 4;
then (the_Source_of G) . e in V by Def29;
hence ((the_Source_of G) | E') . e in V by A3, FUNCT_1:72; :: thesis: verum

end;

then reconsider S = (the_Source_of G) | E' as Function of E',V' by A2, FUNCT_2:5;

now

let e be set ; :: thesis: ( e in E' implies ((the_Target_of G) | E') . e in V )
assume A4: e in E' ; :: thesis: ((the_Target_of G) | E') . e in V
then e in G .edgesInto V by A1, XBOOLE_0:def 4;
then (the_Target_of G) . e in V by Def28;
hence ((the_Target_of G) | E') . e in V by A4, FUNCT_1:72; :: thesis: verum

end;

then reconsider T = (the_Target_of G) | E' as Function of E',V' by A2, FUNCT_2:5;
set IT = createGraph V',E',S,T;
A5: ( the_Vertices_of (createGraph V',E',S,T) = V & the_Edges_of (createGraph V',E',S,T) = E & the_Source_of (createGraph V',E',S,T) = S & the_Target_of (createGraph V',E',S,T) = T ) by FINSEQ_4:91;
then for e being set st e in the_Edges_of (createGraph V',E',S,T) holds
( (the_Source_of (createGraph V',E',S,T)) . e = (the_Source_of G) . e & (the_Target_of (createGraph V',E',S,T)) . e = (the_Target_of G) . e ) by FUNCT_1:72;
then reconsider IT = createGraph V',E',S,T as Subgraph of G by A5, Def34;
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 ) by FINSEQ_4:91; :: thesis: verum

end;

G is Subgraph of G by Lm4;
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