let x be _Graph; :: according to GLPACY00:def 5 :: thesis: ( x in {P1,P2} implies x is Path-like )
assume x in {P1,P2} ; :: thesis: x is Path-like

per cases then ( x = P1 or x = P2 ) by TARSKI:def 2;

suppose x = P1 ; :: thesis: x is Path-like

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

end;

suppose x = P2 ; :: thesis: x is Path-like

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

end;

end;