sqrt 0_No < sqrt x by Th27, SURREALI:def 8;
hence sqrt x is positive ; :: thesis: verum