let G be _Graph; :: thesis: for v being Vertex of G
for C being inducedSubgraph of G,{v} st v is isolated holds
C is Component of G
let v be Vertex of G; :: thesis: for C being inducedSubgraph of G,{v} st v is isolated holds
C is Component of G
let C be inducedSubgraph of G,{v}; :: thesis: ( v is isolated implies C is Component of G )
assume v is isolated ; :: thesis: C is Component of G
then {v} = G .reachableFrom v by Th55;
hence C is Component of G ; :: thesis: verum