reconsider r = x, s = y as positive Real by Th1;
reconsider t = s / r as positive Real ;
t is Element of REALPLUS by Th1;
hence ex b₁ being Element of REALPLUS ex r, s being positive Real st
( x = r & s = y & b₁ = s / r ) ; :: thesis: verum