let a, b, c, d be real number ; :: thesis: ( a <= b & c <= d implies N-bound (closed_inside_of_rectangle a,b,c,d) = d )
assume A1: ( a <= b & c <= d ) ; :: thesis: N-bound (closed_inside_of_rectangle a,b,c,d) = d
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: for p being real number st p in Z holds
p <= d

proof

let p be real number ; :: thesis: ( p in Z implies p <= d )
assume p in Z ; :: thesis: p <= d
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 = (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, A4;
hence p <= d by A2, A4, A5, PSCOMP_1:70; :: thesis: verum

end;

A6: for q being real number st ( for p being real number st p in Z holds
p <= q ) holds
d <= q

proof

let q be real number ; :: thesis: ( ( for p being real number st p in Z holds
p <= q ) implies d <= q )
assume A7: for p being real number st p in Z holds
p <= q ; :: thesis: d <= 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 (proj2 | (closed_inside_of_rectangle a,b,c,d)) . |[b,d]| = |[b,d]| `2 by PSCOMP_1:70;
hence d <= 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 N-bound (closed_inside_of_rectangle a,b,c,d) = d by A3, A6, SEQ_4:63; :: thesis: verum