set S0 = sqrt_0 x;
A1: sqrt_0 x = [(L_ (sqrt_0 x)),(R_ (sqrt_0 x))] ;
A2: sqrt x = [(L_ (sqrt x)),(R_ (sqrt x))] ;
A3: sqrt x = [(Union (sqrtL ((sqrt_0 x),x))),(Union (sqrtR ((sqrt_0 x),x)))] by Th15;
A4: ( L_ (sqrt_0 x) = (sqrtL ((sqrt_0 x),x)) . 0 & (sqrtL ((sqrt_0 x),x)) . 0 c= Union (sqrtL ((sqrt_0 x),x)) & R_ (sqrt_0 x) = (sqrtR ((sqrt_0 x),x)) . 0 & (sqrtR ((sqrt_0 x),x)) . 0 c= Union (sqrtR ((sqrt_0 x),x)) ) by Th6, ABCMIZ_1:1;
then ( L_ (sqrt_0 x) c= L_ (sqrt x) & R_ (sqrt_0 x) c= R_ (sqrt x) ) by A3;
then A5: ( L_ (sqrt_0 x) is surreal-membered & R_ (sqrt_0 x) is surreal-membered ) by SURREAL0:def 16;
( L_ (sqrt_0 x) <=_ L_ (sqrt x) & R_ (sqrt_0 x) <=_ R_ (sqrt x) ) by A4, A3;
hence sqrt_0 x is surreal by A5, A1, A2, SURREALI:37; :: thesis: verum