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