let a, b, c, d be Real; :: thesis: ( a <= b & c <= d implies S-bound (rectangle (a,b,c,d)) = c )

assume that

A1: a <= b and

A2: 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 ;

A3: rectangle (a,b,c,d) = the carrier of ((TOP-REAL 2) | (rectangle (a,b,c,d))) by PRE_TOPC:8;

A4: for p being Real st p in Z holds

p >= c

p >= q ) holds

c >= q

.= lower_bound Z by PSCOMP_1:def 1

.= c by A4, A7, SEQ_4:44 ; :: thesis: verum

assume that

A1: a <= b and

A2: 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 ;

A3: rectangle (a,b,c,d) = the carrier of ((TOP-REAL 2) | (rectangle (a,b,c,d))) by PRE_TOPC:8;

A4: for p being Real st p in Z holds

p >= c

proof

A7:
for q being Real st ( for p being Real st p in Z holds
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

A5: 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

A6: p = (proj2 | (rectangle (a,b,c,d))) . p0 by FUNCT_2:64;

reconsider p0 = p0 as Point of (TOP-REAL 2) by A3, A5;

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, A2, SPPOL_2:54;

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 A3, A5;

hence p >= c by A2, A3, A5, A6, PSCOMP_1:23; :: thesis: verum

end;assume p in Z ; :: thesis: p >= c

then consider p0 being object such that

A5: 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

A6: p = (proj2 | (rectangle (a,b,c,d))) . p0 by FUNCT_2:64;

reconsider p0 = p0 as Point of (TOP-REAL 2) by A3, A5;

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, A2, SPPOL_2:54;

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 A3, A5;

hence p >= c by A2, A3, A5, A6, PSCOMP_1:23; :: thesis: verum

p >= q ) holds

c >= q

proof

thus S-bound (rectangle (a,b,c,d)) =
lower_bound (proj2 | (rectangle (a,b,c,d)))
by PSCOMP_1:def 10
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

|[b,c]| in LSeg (|[b,c]|,|[b,d]|) by RLTOPSP1:68;

then A9: |[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 A10: |[b,c]| in rectangle (a,b,c,d) by A9, XBOOLE_0:def 3;

then (proj2 | (rectangle (a,b,c,d))) . |[b,c]| = |[b,c]| `2 by PSCOMP_1:23

.= c by EUCLID:52 ;

hence c >= q by A3, A8, A10, FUNCT_2:35; :: thesis: verum

end;p >= q ) implies c >= q )

assume A8: for p being Real st p in Z holds

p >= q ; :: thesis: c >= q

|[b,c]| in LSeg (|[b,c]|,|[b,d]|) by RLTOPSP1:68;

then A9: |[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 A10: |[b,c]| in rectangle (a,b,c,d) by A9, XBOOLE_0:def 3;

then (proj2 | (rectangle (a,b,c,d))) . |[b,c]| = |[b,c]| `2 by PSCOMP_1:23

.= c by EUCLID:52 ;

hence c >= q by A3, A8, A10, FUNCT_2:35; :: thesis: verum

.= lower_bound Z by PSCOMP_1:def 1

.= c by A4, A7, SEQ_4:44 ; :: thesis: verum