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;
( ( 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
;
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;
verum
end;
for p being Real st p in Z holds
p <= 1
hence
E-bound R^2-unit_square = 1
by A2, SEQ_4:46; verum