theorem :: REALALG3:42

Positives(F_Rat) extends_to FAdj (F_Rat,{(sqrt (2. F_Rat))})