set PT = { p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2,V } ;
{ p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2,V } c= the carrier' of G *

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2,V } or e in the carrier' of G * )
assume e in { p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2,V } ; :: thesis: e in the carrier' of G *
then ex p being oriented Simple Chain of G st
( e = p & p is_acyclicpath_of v1,v2,V ) ;
hence e in the carrier' of G * by FINSEQ_1:def 11; :: thesis: verum

end;

hence { p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2,V } is Subset of ( the carrier' of G *) ; :: thesis: verum