let a, b, c, d be Real; ( a <= b & c <= d implies S-bound (closed_inside_of_rectangle (a,b,c,d)) = c )
assume that
A1:
a <= b
and
A2:
c <= d
; 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 ;
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:
|[a,c]| in closed_inside_of_rectangle (a,b,c,d)
by A1, A2, TOPREALA:31;
A5:
for p being Real st p in Z holds
p >= c
proof
let p be
Real;
( p in Z implies p >= c )
assume
p in Z
;
p >= c
then consider p0 being
object such that A6:
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 A7:
p = (proj2 | (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, A6;
hence
p >= c
by A3, A6, A7, PSCOMP_1:23;
verum
end;
for q being Real st ( for p being Real st p in Z holds
p >= q ) holds
c >= q
proof
let q be
Real;
( ( for p being Real st p in Z holds
p >= q ) implies c >= q )
assume A8:
for
p being
Real st
p in Z holds
p >= q
;
c >= q
A9:
|[a,c]| `2 = c
by EUCLID:52;
(proj2 | (closed_inside_of_rectangle (a,b,c,d))) . |[a,c]| = |[a,c]| `2
by A1, A2, PSCOMP_1:23, TOPREALA:31;
hence
c >= q
by A3, A4, A8, A9, FUNCT_2:35;
verum
end;
hence
S-bound (closed_inside_of_rectangle (a,b,c,d)) = c
by A4, A5, SEQ_4:44; verum