R [*] is_reflexive_in field R by Lm37;
then R [*] is_reflexive_in field (R [*]) by Lm34;
hence for b₁ being Relation st b₁ = R [*] holds
b₁ is reflexive by RELAT_2:def 9; :: thesis: verum