( x <= 0_No or 0_No <= x ) ;
hence sqrt x is surreal by Th19, Th20; :: thesis: verum