let a, b, c, d be real number ; :: thesis: ( a <= b & c <= d implies E-bound (closed_inside_of_rectangle a,b,c,d) = b )
assume A1:
( a <= b & c <= d )
; :: thesis: 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 ;
A2:
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:29;
A3:
for p being real number st p in Z holds
p <= b
proof
let p be
real number ;
:: thesis: ( p in Z implies p <= b )
assume
p in Z
;
:: thesis: p <= b
then consider p0 being
set such that A4:
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 A5:
p = (proj1 | (closed_inside_of_rectangle a,b,c,d)) . p0
by FUNCT_2:115;
ex
p1 being
Point of
(TOP-REAL 2) st
(
p0 = p1 &
a <= p1 `1 &
p1 `1 <= b &
c <= p1 `2 &
p1 `2 <= d )
by A2, A4;
hence
p <= b
by A2, A4, A5, PSCOMP_1:69;
:: thesis: verum
end;
A6:
for q being real number st ( for p being real number st p in Z holds
p <= q ) holds
b <= q
proof
let q be
real number ;
:: thesis: ( ( for p being real number st p in Z holds
p <= q ) implies b <= q )
assume A7:
for
p being
real number st
p in Z holds
p <= q
;
:: thesis: b <= q
A8:
(
|[b,d]| `1 = b &
|[b,d]| `2 = d )
by EUCLID:56;
then A9:
|[b,d]| in closed_inside_of_rectangle a,
b,
c,
d
by A1;
then
(proj1 | (closed_inside_of_rectangle a,b,c,d)) . |[b,d]| = |[b,d]| `1
by PSCOMP_1:69;
hence
b <= q
by A2, A7, A8, A9, FUNCT_2:43;
:: thesis: verum
end;
A10:
|[a,c]| in closed_inside_of_rectangle a,b,c,d
by A1, TOPREALA:52;
not Z is empty
by A10;
hence
E-bound (closed_inside_of_rectangle a,b,c,d) = b
by A3, A6, SEQ_4:63; :: thesis: verum