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 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
0 >= q
proof
let q be
Real;
( ( for p being Real st p in Z holds
p >= q ) implies 0 >= q )
assume A3:
for
p being
Real st
p in Z holds
p >= q
;
0 >= q
|[1,0]| in LSeg (
|[1,0]|,
|[1,1]|)
by RLTOPSP1:68;
then
|[1,0]| in (LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))
by XBOOLE_0:def 3;
then A4:
|[1,0]| in R^2-unit_square
by XBOOLE_0:def 3;
then (proj2 | R^2-unit_square) . |[1,0]| =
|[1,0]| `2
by PSCOMP_1:23
.=
0
by EUCLID:52
;
hence
0 >= q
by A1, A3, A4, FUNCT_2:35;
verum
end;
for p being Real st p in Z holds
p >= 0
hence
S-bound R^2-unit_square = 0
by A2, SEQ_4:44; verum