let G1, G2 be _Graph; :: thesis: for G being GraphMeet of G1,G2 st G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 holds
G is Subgraph of G2
let G be GraphMeet of G1,G2; :: thesis: ( G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 implies G is Subgraph of G2 )
assume ( G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 ) ; :: thesis: G is Subgraph of G2
then consider S being GraphMeetSet such that
A1: ( S = {G1,G2} & G is GraphMeet of S ) by Def30;
G2 is Element of S by A1, TARSKI:def 2;
then G2 is Supergraph of G by A1, Th37;
hence G is Subgraph of G2 by GLIB_006:57; :: thesis: verum