set PT = { q where q is oriented Simple Chain of G : ( q <> {} & the Source of G . (q . 1) = the Source of G . (p . 1) & the Target of G . (q . (len q)) = the Target of G . (p . (len p)) & rng q c= rng p ) } ;
{ q where q is oriented Simple Chain of G : ( q <> {} & the Source of G . (q . 1) = the Source of G . (p . 1) & the Target of G . (q . (len q)) = the Target of G . (p . (len p)) & rng q c= rng p ) } c= the carrier' of G *

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { q where q is oriented Simple Chain of G : ( q <> {} & the Source of G . (q . 1) = the Source of G . (p . 1) & the Target of G . (q . (len q)) = the Target of G . (p . (len p)) & rng q c= rng p ) } or e in the carrier' of G * )
assume e in { q where q is oriented Simple Chain of G : ( q <> {} & the Source of G . (q . 1) = the Source of G . (p . 1) & the Target of G . (q . (len q)) = the Target of G . (p . (len p)) & rng q c= rng p ) } ; :: thesis: e in the carrier' of G *
then ex q being oriented Simple Chain of G st
( e = q & q <> {} & the Source of G . (q . 1) = the Source of G . (p . 1) & the Target of G . (q . (len q)) = the Target of G . (p . (len p)) & rng q c= rng p ) ;
hence e in the carrier' of G * by FINSEQ_1:def 11; :: thesis: verum

end;

hence { q where q is oriented Simple Chain of G : ( q <> {} & the Source of G . (q . 1) = the Source of G . (p . 1) & the Target of G . (q . (len q)) = the Target of G . (p . (len p)) & rng q c= rng p ) } is Subset of ( the carrier' of G *) ; :: thesis: verum