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

A5: now

let x, y be real number ; :: thesis: ( S₁[x] & S₂[y] implies b₁ <= b₂ )
assume that
A6: S₁[x] and
A7: S₂[y] ; :: thesis: b₁ <= b₂

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

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

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

end;

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

then x ^2 <= y ^2 by A6, A7, XXREAL_0:2;
hence x <= y by A7, Th78; :: thesis: verum

end;

end;

end;

consider z being real number such that
A8: for x, y being real number st S₁[x] & S₂[y] holds
( x <= z & z <= y ) from SQUARE_1:sch 1(A5);
take z ; :: thesis: ( 0 <= z & z ^2 = a )
thus 0 <= z by A1, A3, A4, A8; :: thesis: z ^2 = a
assume A9: 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 A9, XXREAL_0:1;

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

then z = 0 by A1, A3, A4, A8;
then consider c being real number such that
A11: 0 < c and
A12: c ^2 < a by A1, A9, Lm1;
thus contradiction by A1, A3, A4, A8, A10, A11, A12; :: thesis: verum

end;

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

set b = a - (z ^2 );
A15: 0 < a - (z ^2 ) by A13, XREAL_1:52;
then 0 < (a - (z ^2 )) / 2 ;
then consider c being real number such that
A16: 0 < c and
A17: c ^2 < (a - (z ^2 )) / 2 by Lm1;
A18: 2 * z <> 0 by A13;
A19: 0 <= 2 * z by A13;
set eps = min c,((a - (z ^2 )) / (4 * z));
0 < 4 * z by A13;
then 0 < (a - (z ^2 )) / (4 * z) by A15;
then A21: 0 < min c,((a - (z ^2 )) / (4 * z)) by A16, XXREAL_0:15;
(min c,((a - (z ^2 )) / (4 * z))) * (2 * z) <= ((a - (z ^2 )) / (2 * (2 * z))) * (2 * z) by A19, 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 A22: (2 * z) * (min c,((a - (z ^2 )) / (4 * z))) <= (a - (z ^2 )) / 2 by A18, XCMPLX_1:88;
(min c,((a - (z ^2 )) / (4 * z))) ^2 <= c ^2 by A21, Th77, XXREAL_0:17;
then A23: (min c,((a - (z ^2 )) / (4 * z))) ^2 <= (a - (z ^2 )) / 2 by A17, XXREAL_0:2;
A24: a = (z ^2 ) + (a - (z ^2 )) ;
A25: (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 )) ;
((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 A22, A23, XREAL_1:9;
then A26: (z + (min c,((a - (z ^2 )) / (4 * z)))) ^2 <= a by A24, A25, XREAL_1:8;
z < z + (min c,((a - (z ^2 )) / (4 * z))) by A21, XREAL_1:31;
hence contradiction by A1, A3, A4, A8, A26; :: thesis: verum

end;

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

set b = (z ^2 ) - a;
A28: 0 < 2 * z by A27;
A29: 2 * z <> 0 by A27;
A30: 0 < (z ^2 ) - a by A27, XREAL_1:52;
set eps = min (((z ^2 ) - a) / (2 * z)),z;
0 < 2 * z by A27;
then 0 < ((z ^2 ) - a) / (2 * z) by A30;
then A32: 0 < min (((z ^2 ) - a) / (2 * z)),z by A27, XXREAL_0:15;
A33: a = (z ^2 ) - ((z ^2 ) - a) ;
A34: (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 )) ;
(min (((z ^2 ) - a) / (2 * z)),z) * (2 * z) <= (((z ^2 ) - a) / (2 * z)) * (2 * z) by A28, XREAL_1:66, XXREAL_0:17;
then A35: (2 * z) * (min (((z ^2 ) - a) / (2 * z)),z) <= (z ^2 ) - a by A29, XCMPLX_1:88;
0 <= (min (((z ^2 ) - a) / (2 * z)),z) ^2 by XREAL_1:65;
then ((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;
then ((2 * z) * (min (((z ^2 ) - a) / (2 * z)),z)) - ((min (((z ^2 ) - a) / (2 * z)),z) ^2 ) <= (z ^2 ) - a by A35, XXREAL_0:2;
then A36: a <= (z - (min (((z ^2 ) - a) / (2 * z)),z)) ^2 by A33, A34, XREAL_1:15;
A37: 0 <= z - (min (((z ^2 ) - a) / (2 * z)),z) by XREAL_1:50, XXREAL_0:17;
z - (min (((z ^2 ) - a) / (2 * z)),z) < z by A32, XREAL_1:46;
hence contradiction by A8, A36, A37; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum