let G1, G2, G be _Graph; :: thesis: ( G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 implies ( G is GraphMeet of G1,G2 iff ( the_Vertices_of G = (the_Vertices_of G1) /\ (the_Vertices_of G2) & the_Edges_of G = (the_Edges_of G1) /\ (the_Edges_of G2) & the_Source_of G = (the_Source_of G1) /\ (the_Source_of G2) & the_Target_of G = (the_Target_of G1) /\ (the_Target_of G2) ) ) )
assume A1: ( G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 ) ; :: thesis: ( G is GraphMeet of G1,G2 iff ( the_Vertices_of G = (the_Vertices_of G1) /\ (the_Vertices_of G2) & the_Edges_of G = (the_Edges_of G1) /\ (the_Edges_of G2) & the_Source_of G = (the_Source_of G1) /\ (the_Source_of G2) & the_Target_of G = (the_Target_of G1) /\ (the_Target_of G2) ) )
hereby :: thesis: ( the_Vertices_of G = (the_Vertices_of G1) /\ (the_Vertices_of G2) & the_Edges_of G = (the_Edges_of G1) /\ (the_Edges_of G2) & the_Source_of G = (the_Source_of G1) /\ (the_Source_of G2) & the_Target_of G = (the_Target_of G1) /\ (the_Target_of G2) implies G is GraphMeet of G1,G2 )
assume G is GraphMeet of G1,G2 ; :: thesis: ( the_Vertices_of G = (the_Vertices_of G1) /\ (the_Vertices_of G2) & the_Edges_of G = (the_Edges_of G1) /\ (the_Edges_of G2) & the_Source_of G = (the_Source_of G1) /\ (the_Source_of G2) & the_Target_of G = (the_Target_of G1) /\ (the_Target_of G2) )
then consider S being GraphMeetSet such that
A2: ( S = {G1,G2} & G is GraphMeet of S ) by A1, Def30;
thus the_Vertices_of G = meet (the_Vertices_of {G1,G2}) by A2, Def29
.= meet {(the_Vertices_of G1),(the_Vertices_of G2)} by Th6
.= (the_Vertices_of G1) /\ (the_Vertices_of G2) by SETFAM_1:11 ; :: thesis: ( the_Edges_of G = (the_Edges_of G1) /\ (the_Edges_of G2) & the_Source_of G = (the_Source_of G1) /\ (the_Source_of G2) & the_Target_of G = (the_Target_of G1) /\ (the_Target_of G2) )
thus the_Edges_of G = meet (the_Edges_of {G1,G2}) by A2, Def29
.= meet {(the_Edges_of G1),(the_Edges_of G2)} by Th6
.= (the_Edges_of G1) /\ (the_Edges_of G2) by SETFAM_1:11 ; :: thesis: ( the_Source_of G = (the_Source_of G1) /\ (the_Source_of G2) & the_Target_of G = (the_Target_of G1) /\ (the_Target_of G2) )
thus the_Source_of G = meet (the_Source_of {G1,G2}) by A2, Def29
.= meet {(the_Source_of G1),(the_Source_of G2)} by Th6
.= (the_Source_of G1) /\ (the_Source_of G2) by SETFAM_1:11 ; :: thesis: the_Target_of G = (the_Target_of G1) /\ (the_Target_of G2)
thus the_Target_of G = meet (the_Target_of {G1,G2}) by A2, Def29
.= meet {(the_Target_of G1),(the_Target_of G2)} by Th6
.= (the_Target_of G1) /\ (the_Target_of G2) by SETFAM_1:11 ; :: thesis: verum
end;
assume A3: ( the_Vertices_of G = (the_Vertices_of G1) /\ (the_Vertices_of G2) & the_Edges_of G = (the_Edges_of G1) /\ (the_Edges_of G2) & the_Source_of G = (the_Source_of G1) /\ (the_Source_of G2) & the_Target_of G = (the_Target_of G1) /\ (the_Target_of G2) ) ; :: thesis: G is GraphMeet of G1,G2
reconsider S = {G1,G2} as GraphMeetSet by A1, Th35;
A4: the_Vertices_of G c= the_Vertices_of G1 by A3, XBOOLE_1:17;
A5: the_Source_of G c= the_Source_of G1 by A3, XBOOLE_1:17;
the_Target_of G c= the_Target_of G1 by A3, XBOOLE_1:17;
then G1 is Supergraph of G by A4, A5, GLIB_006:63;
then A6: G is Subgraph of G1 by GLIB_006:57;
A7: the_Vertices_of G = meet {(the_Vertices_of G1),(the_Vertices_of G2)} by A3, SETFAM_1:11
.= meet (the_Vertices_of S) by Th6 ;
A8: the_Edges_of G = meet {(the_Edges_of G1),(the_Edges_of G2)} by A3, SETFAM_1:11
.= meet (the_Edges_of S) by Th6 ;
A9: the_Source_of G = meet {(the_Source_of G1),(the_Source_of G2)} by A3, SETFAM_1:11
.= meet (the_Source_of S) by Th6 ;
the_Target_of G = meet {(the_Target_of G1),(the_Target_of G2)} by A3, SETFAM_1:11
.= meet (the_Target_of S) by Th6 ;
then G is GraphMeet of S by A7, A8, A9, Def29;
hence G is GraphMeet of G1,G2 by A1, A6, Def30; :: thesis: verum