let P1 be Path-like _Graph; :: thesis: for v being Vertex of P1
for P2 being removeVertex of P1,v st ( v is endvertex or P1 is _trivial ) holds
P2 is Path-like
let v be Vertex of P1; :: thesis: for P2 being removeVertex of P1,v st ( v is endvertex or P1 is _trivial ) holds
P2 is Path-like
let P2 be removeVertex of P1,v; :: thesis: ( ( v is endvertex or P1 is _trivial ) implies P2 is Path-like )
assume ( v is endvertex or P1 is _trivial ) ; :: thesis: P2 is Path-like

per cases then ( ( not P1 is _trivial & v is endvertex ) or P1 is _trivial ) ;

suppose ( not P1 is _trivial & v is endvertex ) ; :: thesis: P2 is Path-like

then P2 is connected by GLIB_002:4;
hence P2 is Path-like ; :: thesis: verum

end;

suppose P1 is _trivial ; :: thesis: P2 is Path-like

hence P2 is Path-like ; :: thesis: verum

end;

end;