consider x being object such that
A3: x is_a_normal_form_of a,R by A1;
x is set by TARSKI:1;
hence ex b₁ being set st b₁ is_a_normal_form_of a,R by A3; :: thesis: verum