defpred S₁[ Real] means ( 0 <= $1 & a <= $1 ^2 );
defpred S₂[ Real] means ( $1 <= 0 or $1 ^2 <= a );
a <= a + 1 by XREAL_1:29;
then A2: 0 + a <= ((a ^2) + a) + (a + 1) by A1, XREAL_1:7;

A3: now :: thesis: for x, y being Real st S₂[x] & S₁[y] holds
x <= y

let x, y be Real; :: thesis: ( S₂[x] & S₁[y] implies b₁ <= b₂ )
assume that
A4: S₂[x] and
A5: S₁[y] ; :: thesis: b₁ <= b₂

per cases ( x <= 0 or not x <= 0 ) ;

suppose x <= 0 ; :: thesis: b₁ <= b₂

hence x <= y by A5; :: thesis: verum

end;

suppose not x <= 0 ; :: thesis: b₁ <= b₂

then x ^2 <= y ^2 by A4, A5, XXREAL_0:2;
hence x <= y by A5, Th16; :: thesis: verum

end;

end;

end;

consider z being Real such that
A6: for x, y being Real st S₂[x] & S₁[y] holds
( x <= z & z <= y ) from SQUARE_1:sch 1(A3);
take z ; :: thesis: ( 0 <= z & z ^2 = a )
A7: (a + 1) ^2 = ((a ^2) + a) + (a + 1) ;
hence 0 <= z by A1, A2, A6; :: thesis: z ^2 = a
assume A8: z ^2 <> a ; :: thesis: contradiction

now :: thesis: contradiction

per cases ( z <= 0 or ( z ^2 < a & not z <= 0 ) or ( a < z ^2 & not z <= 0 ) ) by A8, XXREAL_0:1;

suppose A9: z <= 0 ; :: thesis: contradiction

then z = 0 by A1, A7, A2, A6;
then ex c being Real st
( 0 < c & c ^2 < a ) by A1, A8, Lm1;
hence contradiction by A1, A7, A2, A6, A9; :: thesis: verum

end;

suppose A10: ( z ^2 < a & not z <= 0 ) ; :: thesis: contradiction

set b = a - (z ^2);
A11: 0 < a - (z ^2) by A10, XREAL_1:50;
then consider c being Real such that
A12: 0 < c and
A13: c ^2 < (a - (z ^2)) / 2 by Lm1;
set eps = min (c,((a - (z ^2)) / (4 * z)));
A14: 0 < min (c,((a - (z ^2)) / (4 * z))) by A10, A11, A12, XXREAL_0:15;
then A15: z < z + (min (c,((a - (z ^2)) / (4 * z)))) by XREAL_1:29;
(min (c,((a - (z ^2)) / (4 * z)))) * (2 * z) <= ((a - (z ^2)) / (2 * (2 * z))) * (2 * z) by A10, XREAL_1:64, XXREAL_0:17;
then (min (c,((a - (z ^2)) / (4 * z)))) * (2 * z) <= (((a - (z ^2)) / 2) / (2 * z)) * (2 * z) by XCMPLX_1:78;
then A16: (2 * z) * (min (c,((a - (z ^2)) / (4 * z)))) <= (a - (z ^2)) / 2 by A10, XCMPLX_1:87;
(min (c,((a - (z ^2)) / (4 * z)))) ^2 <= c ^2 by A14, Th15, XXREAL_0:17;
then (min (c,((a - (z ^2)) / (4 * z)))) ^2 <= (a - (z ^2)) / 2 by A13, XXREAL_0:2;
then A17: ((2 * z) * (min (c,((a - (z ^2)) / (4 * z))))) + ((min (c,((a - (z ^2)) / (4 * z)))) ^2) <= ((a - (z ^2)) / 2) + ((a - (z ^2)) / 2) by A16, XREAL_1:7;
A18: (z + (min (c,((a - (z ^2)) / (4 * z))))) ^2 = (z ^2) + (((2 * z) * (min (c,((a - (z ^2)) / (4 * z))))) + ((min (c,((a - (z ^2)) / (4 * z)))) ^2)) ;
a = (z ^2) + (a - (z ^2)) ;
then (z + (min (c,((a - (z ^2)) / (4 * z))))) ^2 <= a by A18, A17, XREAL_1:6;
hence contradiction by A1, A7, A2, A6, A15; :: thesis: verum

end;

suppose A19: ( a < z ^2 & not z <= 0 ) ; :: thesis: contradiction

set b = (z ^2) - a;
set eps = min ((((z ^2) - a) / (2 * z)),z);
A20: (z - (min ((((z ^2) - a) / (2 * z)),z))) ^2 = (z ^2) - (((2 * z) * (min ((((z ^2) - a) / (2 * z)),z))) - ((min ((((z ^2) - a) / (2 * z)),z)) ^2)) ;
0 < (z ^2) - a by A19, XREAL_1:50;
then 0 < min ((((z ^2) - a) / (2 * z)),z) by A19, XXREAL_0:15;
then A21: z - (min ((((z ^2) - a) / (2 * z)),z)) < z by XREAL_1:44;
0 <= (min ((((z ^2) - a) / (2 * z)),z)) ^2 by XREAL_1:63;
then A22: ((2 * z) * (min ((((z ^2) - a) / (2 * z)),z))) - ((min ((((z ^2) - a) / (2 * z)),z)) ^2) <= ((2 * z) * (min ((((z ^2) - a) / (2 * z)),z))) - 0 by XREAL_1:13;
(min ((((z ^2) - a) / (2 * z)),z)) * (2 * z) <= (((z ^2) - a) / (2 * z)) * (2 * z) by A19, XREAL_1:64, XXREAL_0:17;
then (2 * z) * (min ((((z ^2) - a) / (2 * z)),z)) <= (z ^2) - a by A19, XCMPLX_1:87;
then A23: ((2 * z) * (min ((((z ^2) - a) / (2 * z)),z))) - ((min ((((z ^2) - a) / (2 * z)),z)) ^2) <= (z ^2) - a by A22, XXREAL_0:2;
A24: 0 <= z - (min ((((z ^2) - a) / (2 * z)),z)) by XREAL_1:48, XXREAL_0:17;
a = (z ^2) - ((z ^2) - a) ;
then a <= (z - (min ((((z ^2) - a) / (2 * z)),z))) ^2 by A20, A23, XREAL_1:13;
hence contradiction by A6, A24, A21; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum