let a, b, c, d be Real; ( a <= b & c <= d implies E-bound (rectangle (a,b,c,d)) = b )
assume that
A1:
a <= b
and
A2:
c <= d
; E-bound (rectangle (a,b,c,d)) = b
set X = rectangle (a,b,c,d);
reconsider Z = (proj1 | (rectangle (a,b,c,d))) .: the carrier of ((TOP-REAL 2) | (rectangle (a,b,c,d))) as Subset of REAL ;
A3:
rectangle (a,b,c,d) = the carrier of ((TOP-REAL 2) | (rectangle (a,b,c,d)))
by PRE_TOPC:8;
A4:
for p being Real st p in Z holds
p <= b
proof
let p be
Real;
( p in Z implies p <= b )
assume
p in Z
;
p <= b
then consider p0 being
object such that A5:
p0 in the
carrier of
((TOP-REAL 2) | (rectangle (a,b,c,d)))
and
p0 in the
carrier of
((TOP-REAL 2) | (rectangle (a,b,c,d)))
and A6:
p = (proj1 | (rectangle (a,b,c,d))) . p0
by FUNCT_2:64;
reconsider p0 =
p0 as
Point of
(TOP-REAL 2) by A3, A5;
rectangle (
a,
b,
c,
d)
= { q where q is Point of (TOP-REAL 2) : ( ( q `1 = a & q `2 <= d & q `2 >= c ) or ( q `1 <= b & q `1 >= a & q `2 = d ) or ( q `1 <= b & q `1 >= a & q `2 = c ) or ( q `1 = b & q `2 <= d & q `2 >= c ) ) }
by A1, A2, SPPOL_2:54;
then
ex
q being
Point of
(TOP-REAL 2) st
(
p0 = q & ( (
q `1 = a &
q `2 <= d &
q `2 >= c ) or (
q `1 <= b &
q `1 >= a &
q `2 = d ) or (
q `1 <= b &
q `1 >= a &
q `2 = c ) or (
q `1 = b &
q `2 <= d &
q `2 >= c ) ) )
by A3, A5;
hence
p <= b
by A1, A3, A5, A6, PSCOMP_1:22;
verum
end;
A7:
for q being Real st ( for p being Real st p in Z holds
p <= q ) holds
b <= q
proof
let q be
Real;
( ( for p being Real st p in Z holds
p <= q ) implies b <= q )
assume A8:
for
p being
Real st
p in Z holds
p <= q
;
b <= q
|[b,d]| in LSeg (
|[b,c]|,
|[b,d]|)
by RLTOPSP1:68;
then A9:
|[b,d]| in (LSeg (|[a,c]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[b,d]|))
by XBOOLE_0:def 3;
rectangle (
a,
b,
c,
d)
= ((LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|))) \/ ((LSeg (|[a,c]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[b,d]|)))
by SPPOL_2:def 3;
then A10:
|[b,d]| in rectangle (
a,
b,
c,
d)
by A9, XBOOLE_0:def 3;
then (proj1 | (rectangle (a,b,c,d))) . |[b,d]| =
|[b,d]| `1
by PSCOMP_1:22
.=
b
by EUCLID:52
;
hence
b <= q
by A3, A8, A10, FUNCT_2:35;
verum
end;
thus E-bound (rectangle (a,b,c,d)) =
upper_bound (proj1 | (rectangle (a,b,c,d)))
by PSCOMP_1:def 9
.=
upper_bound Z
by PSCOMP_1:def 2
.=
b
by A4, A7, SEQ_4:46
; verum