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

A3: now

let x, y be real number ; :: 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, Th78; :: thesis: verum

end;

end;

end;

consider z being real number such that
A6: for x, y being real number 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

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 number 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:52;
then consider c being real number 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:31;
(min c,((a - (z ^2 )) / (4 * z))) * (2 * z) <= ((a - (z ^2 )) / (2 * (2 * z))) * (2 * z) by A10, XREAL_1:66, XXREAL_0:17;
then (min c,((a - (z ^2 )) / (4 * z))) * (2 * z) <= (((a - (z ^2 )) / 2) / (2 * z)) * (2 * z) by XCMPLX_1:79;
then A16: (2 * z) * (min c,((a - (z ^2 )) / (4 * z))) <= (a - (z ^2 )) / 2 by A10, XCMPLX_1:88;
(min c,((a - (z ^2 )) / (4 * z))) ^2 <= c ^2 by A14, Th77, 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:9;
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:8;
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:52;
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:46;
0 <= (min (((z ^2 ) - a) / (2 * z)),z) ^2 by XREAL_1:65;
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:15;
(min (((z ^2 ) - a) / (2 * z)),z) * (2 * z) <= (((z ^2 ) - a) / (2 * z)) * (2 * z) by A19, XREAL_1:66, XXREAL_0:17;
then (2 * z) * (min (((z ^2 ) - a) / (2 * z)),z) <= (z ^2 ) - a by A19, XCMPLX_1:88;
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:50, 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:15;
hence contradiction by A6, A24, A21; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum