let G be _Graph; :: thesis: for v being Vertex of G st v is isolated holds
{v} = G .reachableFrom v
let v be Vertex of G; :: thesis: ( v is isolated implies {v} = G .reachableFrom v )
assume A1: v is isolated ; :: thesis: {v} = G .reachableFrom v
for x being object holds
( x in {v} iff x in G .reachableFrom v )
proof
let x be object ; :: thesis: ( x in {v} iff x in G .reachableFrom v )
hereby :: thesis: ( x in G .reachableFrom v implies x in {v} )
assume x in {v} ; :: thesis: x in G .reachableFrom v
then x = v by TARSKI:def 1;
hence x in G .reachableFrom v by GLIB_002:9; :: thesis: verum
end;
assume A2: x in G .reachableFrom v ; :: thesis: x in {v}
then reconsider v2 = x as Vertex of G ;
v = v2 by A1, A2, Th53;
hence x in {v} by TARSKI:def 1; :: thesis: verum
end;
hence {v} = G .reachableFrom v by TARSKI:2; :: thesis: verum