2. F_Rat = 2 '*' (1. F_Rat) by RING_5:2;
hence Positives(F_Rat) extends_to FAdj (F_Rat,{(sqrt (2. F_Rat))}) by REALALG2:19, oext2; :: thesis: verum