let V1 be non empty set ; :: thesis: for V2 being non empty Subset of V1
for E1 being Relation of V1
for E2 being Relation of V2 st E2 c= E1 holds
createGraph (V2,E2) is inducedSubgraph of createGraph (V1,E1),V2,E2
let V2 be non empty Subset of V1; :: thesis: for E1 being Relation of V1
for E2 being Relation of V2 st E2 c= E1 holds
createGraph (V2,E2) is inducedSubgraph of createGraph (V1,E1),V2,E2
let E1 be Relation of V1; :: thesis: for E2 being Relation of V2 st E2 c= E1 holds
createGraph (V2,E2) is inducedSubgraph of createGraph (V1,E1),V2,E2
let E2 be Relation of V2; :: thesis: ( E2 c= E1 implies createGraph (V2,E2) is inducedSubgraph of createGraph (V1,E1),V2,E2 )
assume A1: E2 c= E1 ; :: thesis: createGraph (V2,E2) is inducedSubgraph of createGraph (V1,E1),V2,E2
set G1 = createGraph (V1,E1);
set G2 = createGraph (V2,E2);
A2: ( the_Vertices_of (createGraph (V2,E2)) = V2 & the_Edges_of (createGraph (V2,E2)) = E2 ) ;
A3: V2 is non empty Subset of (the_Vertices_of (createGraph (V1,E1))) ;

now :: thesis: for e being object st e in E2 holds
e in (createGraph (V1,E1)) .edgesBetween V2

let e be object ; :: thesis: ( e in E2 implies e in (createGraph (V1,E1)) .edgesBetween V2 )
set v = (the_Source_of (createGraph (V2,E2))) . e;
set w = (the_Target_of (createGraph (V2,E2))) . e;
assume A4: e in E2 ; :: thesis: e in (createGraph (V1,E1)) .edgesBetween V2
then e in the_Edges_of (createGraph (V2,E2)) ;
then A5: e DJoins (the_Source_of (createGraph (V2,E2))) . e,(the_Target_of (createGraph (V2,E2))) . e, createGraph (V2,E2) by GLIB_000:def 14;
then e Joins (the_Source_of (createGraph (V2,E2))) . e,(the_Target_of (createGraph (V2,E2))) . e, createGraph (V2,E2) by GLIB_000:16;
then ( (the_Source_of (createGraph (V2,E2))) . e in the_Vertices_of (createGraph (V2,E2)) & (the_Target_of (createGraph (V2,E2))) . e in the_Vertices_of (createGraph (V2,E2)) ) by GLIB_000:13;
then A6: ( (the_Source_of (createGraph (V2,E2))) . e in V2 & (the_Target_of (createGraph (V2,E2))) . e in V2 ) ;
e = [((the_Source_of (createGraph (V2,E2))) . e),((the_Target_of (createGraph (V2,E2))) . e)] by A5, Th64;
then e DJoins (the_Source_of (createGraph (V2,E2))) . e,(the_Target_of (createGraph (V2,E2))) . e, createGraph (V1,E1) by A1, A4, Th63;
then ( e in the_Edges_of (createGraph (V1,E1)) & (the_Source_of (createGraph (V1,E1))) . e = (the_Source_of (createGraph (V2,E2))) . e & (the_Target_of (createGraph (V1,E1))) . e = (the_Target_of (createGraph (V2,E2))) . e ) by GLIB_000:def 14;
hence e in (createGraph (V1,E1)) .edgesBetween V2 by A6, GLIB_000:31; :: thesis: verum

end;

then A7: E2 c= (createGraph (V1,E1)) .edgesBetween V2 by TARSKI:def 3;
createGraph (V2,E2) is Subgraph of createGraph (V1,E1)

proof

A9: the_Edges_of (createGraph (V2,E2)) c= the_Edges_of (createGraph (V1,E1)) by A1;

now :: thesis: for e being set st e in the_Edges_of (createGraph (V2,E2)) holds
( (the_Source_of (createGraph (V2,E2))) . e = (the_Source_of (createGraph (V1,E1))) . e & (the_Target_of (createGraph (V2,E2))) . e = (the_Target_of (createGraph (V1,E1))) . e )

let e be set ; :: thesis: ( e in the_Edges_of (createGraph (V2,E2)) implies ( (the_Source_of (createGraph (V2,E2))) . e = (the_Source_of (createGraph (V1,E1))) . e & (the_Target_of (createGraph (V2,E2))) . e = (the_Target_of (createGraph (V1,E1))) . e ) )
assume A10: e in the_Edges_of (createGraph (V2,E2)) ; :: thesis: ( (the_Source_of (createGraph (V2,E2))) . e = (the_Source_of (createGraph (V1,E1))) . e & (the_Target_of (createGraph (V2,E2))) . e = (the_Target_of (createGraph (V1,E1))) . e )
set v = (the_Source_of (createGraph (V2,E2))) . e;
set w = (the_Target_of (createGraph (V2,E2))) . e;
e DJoins (the_Source_of (createGraph (V2,E2))) . e,(the_Target_of (createGraph (V2,E2))) . e, createGraph (V2,E2) by A10, GLIB_000:def 14;
then A11: e = [((the_Source_of (createGraph (V2,E2))) . e),((the_Target_of (createGraph (V2,E2))) . e)] by Th64;
e in E2 by A10;
then e DJoins (the_Source_of (createGraph (V2,E2))) . e,(the_Target_of (createGraph (V2,E2))) . e, createGraph (V1,E1) by A1, A11, Th63;
hence ( (the_Source_of (createGraph (V2,E2))) . e = (the_Source_of (createGraph (V1,E1))) . e & (the_Target_of (createGraph (V2,E2))) . e = (the_Target_of (createGraph (V1,E1))) . e ) by GLIB_000:def 14; :: thesis: verum

end;

hence createGraph (V2,E2) is Subgraph of createGraph (V1,E1) by A9, GLIB_000:def 32; :: thesis: verum

end;

hence createGraph (V2,E2) is inducedSubgraph of createGraph (V1,E1),V2,E2 by A2, A3, A7, GLIB_000:def 37; :: thesis: verum