let a, b, c, d be Real; :: thesis: ( 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 ; :: 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 ;
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; :: thesis: ( p in Z implies p >= c )
assume p in Z ; :: thesis: 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; :: thesis: 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; :: thesis: ( ( 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 ; :: thesis: 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; :: thesis: verum

end;

hence S-bound (closed_inside_of_rectangle (a,b,c,d)) = c by A4, A5, SEQ_4:44; :: thesis: verum