the plain Component of G in G .allComponents() by Th189;
hence not G .allComponents() is empty ; :: thesis: ( G .allComponents() is vertex-disjoint & G .allComponents() is edge-disjoint & G .allComponents() is \/-tolerating & G .allComponents() is plain & G .allComponents() is connected )

now :: thesis: for G1, G2 being _Graph st G1 in G .allComponents() & G2 in G .allComponents() & G1 <> G2 holds
the_Vertices_of G1 misses the_Vertices_of G2

let G1, G2 be _Graph; :: thesis: ( G1 in G .allComponents() & G2 in G .allComponents() & G1 <> G2 implies the_Vertices_of G1 misses the_Vertices_of G2 )
set V1 = the_Vertices_of G1;
set V2 = the_Vertices_of G2;
assume A1: ( G1 in G .allComponents() & G2 in G .allComponents() & G1 <> G2 ) ; :: thesis: the_Vertices_of G1 misses the_Vertices_of G2
then ( the_Vertices_of G1 in the_Vertices_of (G .allComponents()) & the_Vertices_of G2 in the_Vertices_of (G .allComponents()) ) by GLIB_014:def 14;
then A2: ( the_Vertices_of G1 in G .componentSet() & the_Vertices_of G2 in G .componentSet() ) by Lm3;
A3: G .componentSet() is a_partition of the_Vertices_of G by GLIB_008:23;
the_Vertices_of G1 <> the_Vertices_of G2

proof

assume A4: the_Vertices_of G1 = the_Vertices_of G2 ; :: thesis: contradiction
( G1 is Component of G & G2 is Component of G ) by A1, Th189;
hence contradiction by A1, A4, GLIB_002:32, GLIB_009:44; :: thesis: verum

end;

hence the_Vertices_of G1 misses the_Vertices_of G2 by A2, A3, EQREL_1:def 4; :: thesis: verum

end;

hence G .allComponents() is vertex-disjoint by GLIB_015:def 18; :: thesis: ( G .allComponents() is edge-disjoint & G .allComponents() is \/-tolerating & G .allComponents() is plain & G .allComponents() is connected )
hence G .allComponents() is edge-disjoint ; :: thesis: ( G .allComponents() is \/-tolerating & G .allComponents() is plain & G .allComponents() is connected )
thus ( G .allComponents() is \/-tolerating & G .allComponents() is plain ) ; :: thesis: G .allComponents() is connected
for H being _Graph st H in G .allComponents() holds
H is connected by Th189;
hence G .allComponents() is connected by GLIB_014:def 9; :: thesis: verum