set PT = { p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2 } ;
{ p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2 } 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 } 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 } ; :: 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 ) ;
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 } is Subset of ( the carrier' of G *) ; :: thesis: verum