let G1, G2 be _Graph; :: thesis: for G being GraphUnion of G1,G2 st G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2 holds
G .order() = (G1 .order()) +` (G2 .order())
let G be GraphUnion of G1,G2; :: thesis: ( G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2 implies G .order() = (G1 .order()) +` (G2 .order()) )
assume A1: ( G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2 ) ; :: thesis: G .order() = (G1 .order()) +` (G2 .order())
then A2: the_Vertices_of G = (the_Vertices_of G1) \/ (the_Vertices_of G2) by GLIB_014:25;
thus G .order() = (G1 .order()) +` (G2 .order()) by A1, A2, CARD_2:35; :: thesis: verum