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 object ; :: 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