let G be _Graph; :: thesis: for G1, G2 being Subgraph of G holds
( not G1 c< G2 or the_Vertices_of G1 c< the_Vertices_of G2 or the_Edges_of G1 c< the_Edges_of G2 )
let G1, G2 be Subgraph of G; :: thesis: ( not G1 c< G2 or the_Vertices_of G1 c< the_Vertices_of G2 or the_Edges_of G1 c< the_Edges_of G2 )
assume A1: G1 c< G2 ; :: thesis: ( the_Vertices_of G1 c< the_Vertices_of G2 or the_Edges_of G1 c< the_Edges_of G2 )
then G1 c= G2 ;
then A2: G1 is Subgraph of G2 ;
then A3: the_Vertices_of G1 c= the_Vertices_of G2 by Def32;
A4: the_Edges_of G1 c= the_Edges_of G2 by A2, Def32;
A5: not G1 == G2 by A1;
now :: thesis: ( the_Vertices_of G1 c< the_Vertices_of G2 or the_Edges_of G1 c< the_Edges_of G2 )
per cases ( the_Vertices_of G1 <> the_Vertices_of G2 or the_Edges_of G1 <> the_Edges_of G2 ) by A5, Th86;
end;
end;
hence ( the_Vertices_of G1 c< the_Vertices_of G2 or the_Edges_of G1 c< the_Edges_of G2 ) ; :: thesis: verum