let G be _Graph; :: thesis: G .allComponents() c= (G .allInducedSG()) /\ (G .allConnectedSG())

now :: thesis: for x being object st x in G .allComponents() holds
x in (G .allInducedSG()) /\ (G .allConnectedSG())

let x be object ; :: thesis: ( x in G .allComponents() implies x in (G .allInducedSG()) /\ (G .allConnectedSG()) )
assume x in G .allComponents() ; :: thesis: x in (G .allInducedSG()) /\ (G .allConnectedSG())
then reconsider C = x as plain Component of G by Th189;
set v = the Vertex of C;
the_Vertices_of C c= the_Vertices_of G ;
then reconsider v = the Vertex of C as Vertex of G by TARSKI:def 3;
set C9 = the plain inducedSubgraph of G,(G .reachableFrom v);
the_Vertices_of the plain inducedSubgraph of G,(G .reachableFrom v) = G .reachableFrom v by GLIB_000:def 37
.= the_Vertices_of C by GLIB_002:33 ;
then C = the plain inducedSubgraph of G,(G .reachableFrom v) by GLIB_002:32, GLIB_009:44;
then ( x in G .allInducedSG() & x in G .allConnectedSG() ) by Th124;
hence x in (G .allInducedSG()) /\ (G .allConnectedSG()) by XBOOLE_0:def 4; :: thesis: verum

end;

hence G .allComponents() c= (G .allInducedSG()) /\ (G .allConnectedSG()) by TARSKI:def 3; :: thesis: verum