let G, G1 be _Graph; :: thesis: for G2 being Subgraph of G1 holds
( G is GraphMeet of G1,G2 iff G == G2 )
let G2 be Subgraph of G1; :: thesis: ( G is GraphMeet of G1,G2 iff G == G2 )
A1: ( G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 ) by Th15, XBOOLE_1:69;
G1 is Supergraph of G2 by GLIB_006:57;
then A2: ( the_Source_of G2 c= the_Source_of G1 & the_Target_of G2 c= the_Target_of G1 ) by GLIB_006:64;
hereby :: thesis: ( G == G2 implies G is GraphMeet of G1,G2 )
assume A3: G is GraphMeet of G1,G2 ; :: thesis: G == G2
then A4: the_Vertices_of G = (the_Vertices_of G1) /\ (the_Vertices_of G2) by A1, Th40
.= the_Vertices_of G2 by XBOOLE_1:28 ;
A5: the_Edges_of G = (the_Edges_of G1) /\ (the_Edges_of G2) by A1, A3, Th40
.= the_Edges_of G2 by XBOOLE_1:28 ;
A6: the_Source_of G = (the_Source_of G1) /\ (the_Source_of G2) by A1, A3, Th40
.= the_Source_of G2 by A2, XBOOLE_1:28 ;
the_Target_of G = (the_Target_of G1) /\ (the_Target_of G2) by A1, A3, Th40
.= the_Target_of G2 by A2, XBOOLE_1:28 ;
hence G == G2 by A4, A5, A6, GLIB_000:def 34; :: thesis: verum
end;
assume A7: G == G2 ; :: thesis: G is GraphMeet of G1,G2
then A8: the_Vertices_of G = the_Vertices_of G2 by GLIB_000:def 34
.= (the_Vertices_of G1) /\ (the_Vertices_of G2) by XBOOLE_1:28 ;
A9: the_Edges_of G = the_Edges_of G2 by A7, GLIB_000:def 34
.= (the_Edges_of G1) /\ (the_Edges_of G2) by XBOOLE_1:28 ;
A10: the_Source_of G = the_Source_of G2 by A7, GLIB_000:def 34
.= (the_Source_of G1) /\ (the_Source_of G2) by A2, XBOOLE_1:28 ;
the_Target_of G = the_Target_of G2 by A7, GLIB_000:def 34
.= (the_Target_of G1) /\ (the_Target_of G2) by A2, XBOOLE_1:28 ;
hence G is GraphMeet of G1,G2 by A1, A8, A9, A10, Th40; :: thesis: verum