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