R [*] is_transitive_in field R by Lm31;
then R [*] is_transitive_in field (R [*]) by Lm34;
hence for b₁ being Relation st b₁ = R [*] holds
b₁ is transitive by RELAT_2:def 16; :: thesis: verum