let a, b, c, d be real number ; :: thesis: ( a <= b & c <= d implies S-bound (rectangle a,b,c,d) = c )
assume A1: ( a <= b & c <= d ) ; :: thesis: S-bound (rectangle a,b,c,d) = c
set X = rectangle a,b,c,d;
reconsider Z = (proj2 | (rectangle a,b,c,d)) .: the carrier of ((TOP-REAL 2) | (rectangle a,b,c,d)) as Subset of REAL ;
A2: rectangle a,b,c,d = the carrier of ((TOP-REAL 2) | (rectangle a,b,c,d)) by PRE_TOPC:29;
A3: 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
A4: p0 in the carrier of ((TOP-REAL 2) | (rectangle a,b,c,d)) and
p0 in the carrier of ((TOP-REAL 2) | (rectangle a,b,c,d)) and
A5: p = (proj2 | (rectangle a,b,c,d)) . p0 by FUNCT_2:115;
reconsider p0 = p0 as Point of (TOP-REAL 2) by A2, A4;
rectangle a,b,c,d = { q where q is Point of (TOP-REAL 2) : ( ( q `1 = a & q `2 <= d & q `2 >= c ) or ( q `1 <= b & q `1 >= a & q `2 = d ) or ( q `1 <= b & q `1 >= a & q `2 = c ) or ( q `1 = b & q `2 <= d & q `2 >= c ) ) } by A1, SPPOL_2:58;
then ex q being Point of (TOP-REAL 2) st
( p0 = q & ( ( q `1 = a & q `2 <= d & q `2 >= c ) or ( q `1 <= b & q `1 >= a & q `2 = d ) or ( q `1 <= b & q `1 >= a & q `2 = c ) or ( q `1 = b & q `2 <= d & q `2 >= c ) ) ) by A2, A4;
hence p >= c by A1, 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
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 A7: for p being real number st p in Z holds
p >= q ; :: thesis: c >= q
|[b,c]| in LSeg |[b,c]|,|[b,d]| by TOPREAL1:6;
then A8: |[b,c]| in (LSeg |[a,c]|,|[b,c]|) \/ (LSeg |[b,c]|,|[b,d]|) by XBOOLE_0:def 3;
rectangle a,b,c,d = ((LSeg |[a,c]|,|[a,d]|) \/ (LSeg |[a,d]|,|[b,d]|)) \/ ((LSeg |[a,c]|,|[b,c]|) \/ (LSeg |[b,c]|,|[b,d]|)) by SPPOL_2:def 3;
then A9: |[b,c]| in rectangle a,b,c,d by A8, XBOOLE_0:def 3;
then (proj2 | (rectangle a,b,c,d)) . |[b,c]| = |[b,c]| `2 by PSCOMP_1:70
.= c by EUCLID:56 ;
hence c >= q by A2, A7, A9, FUNCT_2:43; :: thesis: verum

end;

thus S-bound (rectangle a,b,c,d) = inf (proj2 | (rectangle a,b,c,d)) by PSCOMP_1:def 33
.= lower_bound Z by PSCOMP_1:def 20
.= c by A3, A6, SEQ_4:61 ; :: thesis: verum