let G1 be _Graph; :: thesis: for G2 being Subgraph of G1
for G3 being Subgraph of G2 holds G3 is Subgraph of G1
let G2 be Subgraph of G1; :: thesis: for G3 being Subgraph of G2 holds G3 is Subgraph of G1
let G3 be Subgraph of G2; :: thesis: G3 is Subgraph of G1
A1: the_Edges_of G2 c= the_Edges_of G1 ;
A2: the_Vertices_of G3 c= the_Vertices_of G2 ;
now :: thesis: ( the_Vertices_of G3 c= the_Vertices_of G1 & the_Edges_of G3 c= the_Edges_of G1 & ( for e being set st e in the_Edges_of G3 holds
( (the_Source_of G3) . e = (the_Source_of G1) . e & (the_Target_of G3) . e = (the_Target_of G1) . e ) ) )
thus the_Vertices_of G3 c= the_Vertices_of G1 by A2, XBOOLE_1:1; :: thesis: ( the_Edges_of G3 c= the_Edges_of G1 & ( for e being set st e in the_Edges_of G3 holds
( (the_Source_of G3) . e = (the_Source_of G1) . e & (the_Target_of G3) . e = (the_Target_of G1) . e ) ) )
thus the_Edges_of G3 c= the_Edges_of G1 by A1; :: thesis: for e being set st e in the_Edges_of G3 holds
( (the_Source_of G3) . e = (the_Source_of G1) . e & (the_Target_of G3) . e = (the_Target_of G1) . e )
let e be set ; :: thesis: ( e in the_Edges_of G3 implies ( (the_Source_of G3) . e = (the_Source_of G1) . e & (the_Target_of G3) . e = (the_Target_of G1) . e ) )
assume A3: e in the_Edges_of G3 ; :: thesis: ( (the_Source_of G3) . e = (the_Source_of G1) . e & (the_Target_of G3) . e = (the_Target_of G1) . e )
hence (the_Source_of G3) . e = (the_Source_of G2) . e by Def32
.= (the_Source_of G1) . e by A3, Def32 ;
:: thesis: (the_Target_of G3) . e = (the_Target_of G1) . e
thus (the_Target_of G3) . e = (the_Target_of G2) . e by A3, Def32
.= (the_Target_of G1) . e by A3, Def32 ; :: thesis: verum
end;
hence G3 is Subgraph of G1 by Def32; :: thesis: verum