let G, G1 be _Graph; :: thesis: for G2 being Subgraph of G1 holds
( G is GraphUnion of G1,G2 iff G == G1 )
let G2 be Subgraph of G1; :: thesis: ( G is GraphUnion of G1,G2 iff G == G1 )
A1: G1 tolerates G2 by Th15;
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 == G1 implies G is GraphUnion of G1,G2 )
assume A3: G is GraphUnion of G1,G2 ; :: thesis: G == G1
then A4: the_Vertices_of G = (the_Vertices_of G1) \/ (the_Vertices_of G2) by A1, Th25
.= the_Vertices_of G1 by XBOOLE_1:12 ;
A5: the_Edges_of G = (the_Edges_of G1) \/ (the_Edges_of G2) by A1, A3, Th25
.= the_Edges_of G1 by XBOOLE_1:12 ;
A6: the_Source_of G = (the_Source_of G1) +* (the_Source_of G2) by A1, A3, Th25
.= (the_Source_of G1) \/ (the_Source_of G2) by A1, FUNCT_4:30
.= the_Source_of G1 by A2, XBOOLE_1:12 ;
the_Target_of G = (the_Target_of G1) +* (the_Target_of G2) by A1, A3, Th25
.= (the_Target_of G1) \/ (the_Target_of G2) by A1, FUNCT_4:30
.= the_Target_of G1 by A2, XBOOLE_1:12 ;
hence G == G1 by A4, A5, A6, GLIB_000:def 34; :: thesis: verum
end;
assume A7: G == G1 ; :: thesis: G is GraphUnion of G1,G2
then A8: the_Vertices_of G = the_Vertices_of G1 by GLIB_000:def 34
.= (the_Vertices_of G1) \/ (the_Vertices_of G2) by XBOOLE_1:12 ;
A9: the_Edges_of G = the_Edges_of G1 by A7, GLIB_000:def 34
.= (the_Edges_of G1) \/ (the_Edges_of G2) by XBOOLE_1:12 ;
A10: the_Source_of G = the_Source_of G1 by A7, GLIB_000:def 34
.= (the_Source_of G1) \/ (the_Source_of G2) by A2, XBOOLE_1:12
.= (the_Source_of G1) +* (the_Source_of G2) by A1, FUNCT_4:30 ;
the_Target_of G = the_Target_of G1 by A7, GLIB_000:def 34
.= (the_Target_of G1) \/ (the_Target_of G2) by A2, XBOOLE_1:12
.= (the_Target_of G1) +* (the_Target_of G2) by A1, FUNCT_4:30 ;
hence G is GraphUnion of G1,G2 by A1, A8, A9, A10, Th25; :: thesis: verum