let a, b, c, d be Real; ( a <= b & c <= d implies E-bound (closed_inside_of_rectangle (a,b,c,d)) = b )
assume that
A1:
a <= b
and
A2:
c <= d
; E-bound (closed_inside_of_rectangle (a,b,c,d)) = b
set X = closed_inside_of_rectangle (a,b,c,d);
reconsider Z = (proj1 | (closed_inside_of_rectangle (a,b,c,d))) .: the carrier of ((TOP-REAL 2) | (closed_inside_of_rectangle (a,b,c,d))) as Subset of REAL ;
A3:
closed_inside_of_rectangle (a,b,c,d) = the carrier of ((TOP-REAL 2) | (closed_inside_of_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) | (closed_inside_of_rectangle (a,b,c,d)))
and
p0 in the
carrier of
((TOP-REAL 2) | (closed_inside_of_rectangle (a,b,c,d)))
and A6:
p = (proj1 | (closed_inside_of_rectangle (a,b,c,d))) . p0
by FUNCT_2:64;
ex
p1 being
Point of
(TOP-REAL 2) st
(
p0 = p1 &
a <= p1 `1 &
p1 `1 <= b &
c <= p1 `2 &
p1 `2 <= d )
by A3, A5;
hence
p <= b
by 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
A9:
|[b,d]| `1 = b
by EUCLID:52;
|[b,d]| `2 = d
by EUCLID:52;
then A10:
|[b,d]| in closed_inside_of_rectangle (
a,
b,
c,
d)
by A1, A2, A9;
then
(proj1 | (closed_inside_of_rectangle (a,b,c,d))) . |[b,d]| = |[b,d]| `1
by PSCOMP_1:22;
hence
b <= q
by A3, A8, A9, A10, FUNCT_2:35;
verum
end;
|[a,c]| in closed_inside_of_rectangle (a,b,c,d)
by A1, A2, TOPREALA:31;
hence
E-bound (closed_inside_of_rectangle (a,b,c,d)) = b
by A4, A7, SEQ_4:46; verum