let G1 be _Graph; :: thesis: for G2 being spanning Subgraph of G1
for G3 being spanning Subgraph of G2 holds G3 is spanning Subgraph of G1
let G2 be spanning Subgraph of G1; :: thesis: for G3 being spanning Subgraph of G2 holds G3 is spanning Subgraph of G1
let G3 be spanning Subgraph of G2; :: thesis: G3 is spanning Subgraph of G1
the_Vertices_of G3 = the_Vertices_of G2 by Def33
.= the_Vertices_of G1 by Def33 ;
hence G3 is spanning Subgraph of G1 by Def33, Th43; :: thesis: verum