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 that
A1: a <= b and
A2: 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 ;
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:29;
A4: 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
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: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 A3, A5;
hence p <= b by A3, A5, A6, PSCOMP_1:69; :: thesis: verum

end;

A7: 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 A8: for p being real number st p in Z holds
p <= q ; :: thesis: b <= q
A9: |[b,d]| `1 = b by EUCLID:56;
|[b,d]| `2 = d by EUCLID:56;
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:69;
hence b <= q by A3, A8, A9, A10, FUNCT_2:43; :: thesis: verum

end;

|[a,c]| in closed_inside_of_rectangle a,b,c,d by A1, A2, TOPREALA:52;
hence E-bound (closed_inside_of_rectangle a,b,c,d) = b by A4, A7, SEQ_4:63; :: thesis: verum