let G be _Graph; :: thesis: for G1, G2 being Subgraph of G holds
( not G1 c< G2 or ex v being object st
( v in the_Vertices_of G2 & not v in the_Vertices_of G1 ) or ex e being object st
( e in the_Edges_of G2 & not e in the_Edges_of G1 ) )
let G1, G2 be Subgraph of G; :: thesis: ( not G1 c< G2 or ex v being object st
( v in the_Vertices_of G2 & not v in the_Vertices_of G1 ) or ex e being object st
( e in the_Edges_of G2 & not e in the_Edges_of G1 ) )
assume G1 c< G2 ; :: thesis: ( ex v being object st
( v in the_Vertices_of G2 & not v in the_Vertices_of G1 ) or ex e being object st
( e in the_Edges_of G2 & not e in the_Edges_of G1 ) )
then ( the_Vertices_of G1 c< the_Vertices_of G2 or the_Edges_of G1 c< the_Edges_of G2 ) by Th98;
hence ( ex v being object st
( v in the_Vertices_of G2 & not v in the_Vertices_of G1 ) or ex e being object st
( e in the_Edges_of G2 & not e in the_Edges_of G1 ) ) by XBOOLE_0:6; :: thesis: verum