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