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 by Def38;
then A2: G1 is Subgraph of G2 by Def37;
then A3: the_Vertices_of G1 c= the_Vertices_of G2 by Def34;
A4: the_Edges_of G1 c= the_Edges_of G2 by A2, Def34;
A5: not G1 == G2 by A1, Def38;

now

per cases ( the_Vertices_of G1 <> the_Vertices_of G2 or the_Edges_of G1 <> the_Edges_of G2 ) by A5, Th89;

suppose the_Vertices_of G1 <> the_Vertices_of G2 ; :: thesis: ( the_Vertices_of G1 c< the_Vertices_of G2 or the_Edges_of G1 c< the_Edges_of G2 )

hence ( the_Vertices_of G1 c< the_Vertices_of G2 or the_Edges_of G1 c< the_Edges_of G2 ) by A3, XBOOLE_0:def 8; :: thesis: verum

end;

suppose the_Edges_of G1 <> the_Edges_of G2 ; :: thesis: ( the_Vertices_of G1 c< the_Vertices_of G2 or the_Edges_of G1 c< the_Edges_of G2 )

hence ( the_Vertices_of G1 c< the_Vertices_of G2 or the_Edges_of G1 c< the_Edges_of G2 ) by A4, XBOOLE_0:def 8; :: thesis: verum

end;

end;

end;

hence ( the_Vertices_of G1 c< the_Vertices_of G2 or the_Edges_of G1 c< the_Edges_of G2 ) ; :: thesis: verum