set X = R^2-unit_square ;
reconsider Z = (proj1 | 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 5
.= the carrier of ((TOP-REAL 2) | R^2-unit_square) ;
A2: for q being Real st ( for p being Real st p in Z holds
p <= q ) holds
1 <= q

proof

let q be Real; :: thesis: ( ( for p being Real st p in Z holds
p <= q ) implies 1 <= q )
assume A3: for p being Real st p in Z holds
p <= q ; :: thesis: 1 <= q
|[1,1]| in LSeg (|[1,0]|,|[1,1]|) by RLTOPSP1:68;
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 (proj1 | R^2-unit_square) . |[1,1]| = |[1,1]| `1 by PSCOMP_1:22
.= 1 by EUCLID:52 ;
hence 1 <= q by A1, A3, A4, FUNCT_2:35; :: thesis: verum

end;

for p being Real st p in Z holds
p <= 1

proof

let p be Real; :: thesis: ( p in Z implies p <= 1 )
assume p in Z ; :: thesis: p <= 1
then consider p0 being object 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 = (proj1 | R^2-unit_square) . p0 by FUNCT_2:64;
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:14;
hence p <= 1 by A1, A5, A6, PSCOMP_1:22; :: thesis: verum

end;

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