set v = the Vertex of G;

set IT = the inducedSubgraph of G,(G .reachableFrom the Vertex of G);

take the inducedSubgraph of G,(G .reachableFrom the Vertex of G) ; :: thesis: the inducedSubgraph of G,(G .reachableFrom the Vertex of G) is Component-like

thus the inducedSubgraph of G,(G .reachableFrom the Vertex of G) is Component-like ; :: thesis: verum

set IT = the inducedSubgraph of G,(G .reachableFrom the Vertex of G);

take the inducedSubgraph of G,(G .reachableFrom the Vertex of G) ; :: thesis: the inducedSubgraph of G,(G .reachableFrom the Vertex of G) is Component-like

thus the inducedSubgraph of G,(G .reachableFrom the Vertex of G) is Component-like ; :: thesis: verum