set IT = { ss where ss is Element of the carrier of g * : ss is_path_of v1,v2 } ;
{ ss where ss is Element of the carrier of g * : ss is_path_of v1,v2 } c= the carrier of g *

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { ss where ss is Element of the carrier of g * : ss is_path_of v1,v2 } or e in the carrier of g * )
assume e in { ss where ss is Element of the carrier of g * : ss is_path_of v1,v2 } ; :: thesis: e in the carrier of g *
then ex ss being Element of the carrier of g * st
( e = ss & ss is_path_of v1,v2 ) ;
hence e in the carrier of g * ; :: thesis: verum

end;

hence { ss where ss is Element of the carrier of g * : ss is_path_of v1,v2 } is Subset of (the carrier of g * ) ; :: thesis: verum