proof of transitivity⊃, new unproven theorems added, some code cleaning