let a, b, c, d be real number ; :: thesis: ( a <= b & c <= d implies S-bound (closed_inside_of_rectangle a,b,c,d) = c )
assume A1:
( a <= b & c <= d )
; :: thesis: S-bound (closed_inside_of_rectangle a,b,c,d) = c
set X = closed_inside_of_rectangle a,b,c,d;
reconsider Z = (proj2 | (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:
|[a,c]| in closed_inside_of_rectangle a,b,c,d
by A1, TOPREALA:52;
A4:
for p being real number st p in Z holds
p >= c
proof
let p be
real number ;
:: thesis: ( p in Z implies p >= c )
assume
p in Z
;
:: thesis: p >= c
then consider p0 being
set 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 = (proj2 | (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, A5;
hence
p >= c
by A2, A5, A6, PSCOMP_1:70;
:: thesis: verum
end;
A7:
for q being real number st ( for p being real number st p in Z holds
p >= q ) holds
c >= q
proof
let q be
real number ;
:: thesis: ( ( for p being real number st p in Z holds
p >= q ) implies c >= q )
assume A8:
for
p being
real number st
p in Z holds
p >= q
;
:: thesis: c >= q
A9:
(
|[a,c]| `1 = a &
|[a,c]| `2 = c )
by EUCLID:56;
(proj2 | (closed_inside_of_rectangle a,b,c,d)) . |[a,c]| = |[a,c]| `2
by A1, PSCOMP_1:70, TOPREALA:52;
hence
c >= q
by A2, A3, A8, A9, FUNCT_2:43;
:: thesis: verum
end;
not Z is empty
by A3;
hence
S-bound (closed_inside_of_rectangle a,b,c,d) = c
by A4, A7, SEQ_4:61; :: thesis: verum