let G be _Graph; :: thesis: for v1, v2 being Vertex of G st v1 is isolated & v1 <> v2 holds
not v2 in G .reachableFrom v1
let v1, v2 be Vertex of G; :: thesis: ( v1 is isolated & v1 <> v2 implies not v2 in G .reachableFrom v1 )
assume A1: ( v1 is isolated & v1 <> v2 ) ; :: thesis: not v2 in G .reachableFrom v1
assume v2 in G .reachableFrom v1 ; :: thesis: contradiction
then consider W being Walk of G such that
A2: W is_Walk_from v1,v2 by GLIB_002:def 5;
A3: ( W .first() = v1 & W .last() = v2 ) by A2, GLIB_001:def 23;
then v1 in W .vertices() by GLIB_001:88;
hence contradiction by A1, A3, GLIB_001:127, GLIB_001:135; :: thesis: verum