theorem :: REALALG3:43

Positives(F_Rat) not_extends_to FAdj (F_Rat,{(sqrt (- (1. F_Rat)))}) by REALALG1:26, oext2;