TC or not?

Given:

fact1-  i:myCar rdf:type c:HondaCivic .
fact2-  c:HondaCivic rdfs:subClassOf c:PassengerVehicle .
fact3-  c:PassengerVehicle rdfs:subClassOf c:ThingThatCanBeInsured .

From fact1 + fact2 + fact3  may i conclude?

result1-   i:myCar rdf:type  c:PassengerVehicle .
result2-   i:myCar rdf:type  c:ThingThatCanBeInsured .

No, because FOL doesnt give me this transitive closure .

So, Lets make it by adding a rule:

rule1 - { ?c rdfs:subClassOf ?sc.  ?i rdf:type ?c . } ->  { ?i rdf:type ?sc }



ASK> i:myCar rdf:type ?WHAT


result1> ?WHAT = c:PassengerVehicle
   proof>
      rule1-             { ?c rdfs:subClassOf ?sc.  ?i rdf:type ?c . } ->  { ?i rdf:type ?sc }
      fact1-              i:myCar rdf:type c:HondaCivic .
      fact2-              c:HondaCivic rdfs:subClassOf c:PassengerVehicle .
      rule1+fact2+fact1   c:HondaCivic rdfs:subClassOf c:PassengerVehicle .  i:myCar rdf:type c:HondaCivic .
      ded1-            -> i:myCar rdf:type c:PassengerVehicle

result2> ?WHAT = c:ThingThatCanBeInsured
   proof>
      rule1-               { ?c rdfs:subClassOf ?sc.  ?i rdf:type ?c . } ->  { ?i rdf:type ?sc }
      fact1-               i:myCar rdf:type c:HondaCivic .
      fact2-               c:HondaCivic rdfs:subClassOf c:PassengerVehicle .
      rule1+fact2+fact1:   c:HondaCivic rdfs:subClassOf c:PassengerVehicle . i:myCar rdf:type c:HondaCivic .
      ded1-              -> i:myCar rdf:type c:PassengerVehicle .
      fact3-               c:PassengerVehicle rdfs:subClassOf c:ThingThatCanBeInsured .
      rule1+ded1+fact3     c:PassengerVehicle rdfs:subClassOf c:ThingThatCanBeInsured .  i:myCar rdf:type c:PassengerVehicle .
      ded2-              -> i:myCar rdf:type c:ThingThatCanBeInsured


Oh, still no TC? Perhaps not.  Since TC would have meant that the proofs would have been the same lengths?