set PT = { q where q is oriented Simple Chain of G : verum } ;
{ q where q is oriented Simple Chain of G : verum } c= the carrier' of G *

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { q where q is oriented Simple Chain of G : verum } or e in the carrier' of G * )
assume e in { q where q is oriented Simple Chain of G : verum } ; :: thesis: e in the carrier' of G *
then ex q being oriented Simple Chain of G st e = q ;
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 : verum } is Subset of (the carrier' of G * ) ; :: thesis: verum