set X = R^2-unit_square ;
reconsider Z = (proj2 | R^2-unit_square ) .: the carrier of ((TOP-REAL 2) | R^2-unit_square ) as Subset of REAL ;
A1: R^2-unit_square = [#] ((TOP-REAL 2) | R^2-unit_square ) by PRE_TOPC:def 10
.= the carrier of ((TOP-REAL 2) | R^2-unit_square ) ;
A2: for q being real number st ( for p being real number st p in Z holds
p <= q ) holds
1 <= q

proof

let q be real number ; :: thesis: ( ( for p being real number st p in Z holds
p <= q ) implies 1 <= q )
assume A3: for p being real number st p in Z holds
p <= q ; :: thesis: 1 <= q
|[1,1]| in LSeg |[1,0 ]|,|[1,1]| by RLTOPSP1:69;
then |[1,1]| in (LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|) by XBOOLE_0:def 3;
then A4: |[1,1]| in R^2-unit_square by XBOOLE_0:def 3;
then (proj2 | R^2-unit_square ) . |[1,1]| = |[1,1]| `2 by PSCOMP_1:70
.= 1 by EUCLID:56 ;
hence 1 <= q by A1, A3, A4, FUNCT_2:43; :: thesis: verum

end;

for p being real number st p in Z holds
p <= 1

proof

let p be real number ; :: thesis: ( p in Z implies p <= 1 )
assume p in Z ; :: thesis: p <= 1
then consider p0 being set such that
A5: p0 in the carrier of ((TOP-REAL 2) | R^2-unit_square ) and
p0 in the carrier of ((TOP-REAL 2) | R^2-unit_square ) and
A6: p = (proj2 | R^2-unit_square ) . p0 by FUNCT_2:115;
reconsider p0 = p0 as Point of (TOP-REAL 2) by A1, A5;
ex q being Point of (TOP-REAL 2) st
( p0 = q & ( ( q `1 = 0 & q `2 <= 1 & q `2 >= 0 ) or ( q `1 <= 1 & q `1 >= 0 & q `2 = 1 ) or ( q `1 <= 1 & q `1 >= 0 & q `2 = 0 ) or ( q `1 = 1 & q `2 <= 1 & q `2 >= 0 ) ) ) by A1, A5, TOPREAL1:20;
hence p <= 1 by A1, A5, A6, PSCOMP_1:70; :: thesis: verum

end;

hence N-bound R^2-unit_square = 1 by A2, SEQ_4:63; :: thesis: verum