let a, b, c, d be Real; :: thesis: ( a <= b & c <= d implies ( W-min (rectangle (a,b,c,d)) = |[a,c]| & E-max (rectangle (a,b,c,d)) = |[b,d]| ) )

set K = rectangle (a,b,c,d);

assume that

A1: a <= b and

A2: c <= d ; :: thesis: ( W-min (rectangle (a,b,c,d)) = |[a,c]| & E-max (rectangle (a,b,c,d)) = |[b,d]| )

A3: lower_bound (proj2 | (LSeg (|[a,c]|,|[a,d]|))) = c

A13: W-bound (rectangle (a,b,c,d)) = a by A1, A2, Th36;

A14: upper_bound (proj2 | (LSeg (|[b,c]|,|[b,d]|))) = d

E-bound (rectangle (a,b,c,d)) = b by A1, A2, Th38;

hence ( W-min (rectangle (a,b,c,d)) = |[a,c]| & E-max (rectangle (a,b,c,d)) = |[b,d]| ) by A3, A12, A13, A14, A23, PSCOMP_1:def 19, PSCOMP_1:def 23; :: thesis: verum

set K = rectangle (a,b,c,d);

assume that

A1: a <= b and

A2: c <= d ; :: thesis: ( W-min (rectangle (a,b,c,d)) = |[a,c]| & E-max (rectangle (a,b,c,d)) = |[b,d]| )

A3: lower_bound (proj2 | (LSeg (|[a,c]|,|[a,d]|))) = c

proof

A12:
W-most (rectangle (a,b,c,d)) = LSeg (|[a,c]|,|[a,d]|)
by A1, A2, Th44;
set X = LSeg (|[a,c]|,|[a,d]|);

reconsider Z = (proj2 | (LSeg (|[a,c]|,|[a,d]|))) .: the carrier of ((TOP-REAL 2) | (LSeg (|[a,c]|,|[a,d]|))) as Subset of REAL ;

A4: LSeg (|[a,c]|,|[a,d]|) = the carrier of ((TOP-REAL 2) | (LSeg (|[a,c]|,|[a,d]|))) by PRE_TOPC:8;

A5: for p being Real st p in Z holds

p >= c

p >= q ) holds

c >= q

.= c by A5, A9, SEQ_4:44 ; :: thesis: verum

end;reconsider Z = (proj2 | (LSeg (|[a,c]|,|[a,d]|))) .: the carrier of ((TOP-REAL 2) | (LSeg (|[a,c]|,|[a,d]|))) as Subset of REAL ;

A4: LSeg (|[a,c]|,|[a,d]|) = the carrier of ((TOP-REAL 2) | (LSeg (|[a,c]|,|[a,d]|))) by PRE_TOPC:8;

A5: for p being Real st p in Z holds

p >= c

proof

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

A6: p0 in the carrier of ((TOP-REAL 2) | (LSeg (|[a,c]|,|[a,d]|))) and

p0 in the carrier of ((TOP-REAL 2) | (LSeg (|[a,c]|,|[a,d]|))) and

A7: p = (proj2 | (LSeg (|[a,c]|,|[a,d]|))) . p0 by FUNCT_2:64;

reconsider p0 = p0 as Point of (TOP-REAL 2) by A4, A6;

A8: |[a,c]| `2 = c by EUCLID:52;

|[a,d]| `2 = d by EUCLID:52;

then p0 `2 >= c by A2, A4, A6, A8, TOPREAL1:4;

hence p >= c by A4, A6, A7, PSCOMP_1:23; :: thesis: verum

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

then consider p0 being object such that

A6: p0 in the carrier of ((TOP-REAL 2) | (LSeg (|[a,c]|,|[a,d]|))) and

p0 in the carrier of ((TOP-REAL 2) | (LSeg (|[a,c]|,|[a,d]|))) and

A7: p = (proj2 | (LSeg (|[a,c]|,|[a,d]|))) . p0 by FUNCT_2:64;

reconsider p0 = p0 as Point of (TOP-REAL 2) by A4, A6;

A8: |[a,c]| `2 = c by EUCLID:52;

|[a,d]| `2 = d by EUCLID:52;

then p0 `2 >= c by A2, A4, A6, A8, TOPREAL1:4;

hence p >= c by A4, A6, A7, PSCOMP_1:23; :: thesis: verum

p >= q ) holds

c >= q

proof

thus lower_bound (proj2 | (LSeg (|[a,c]|,|[a,d]|))) =
lower_bound Z
by PSCOMP_1:def 1
let q be Real; :: thesis: ( ( for p being Real st p in Z holds

p >= q ) implies c >= q )

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

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

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

(proj2 | (LSeg (|[a,c]|,|[a,d]|))) . |[a,c]| = |[a,c]| `2 by PSCOMP_1:23, RLTOPSP1:68

.= c by EUCLID:52 ;

hence c >= q by A4, A10, A11, FUNCT_2:35; :: thesis: verum

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

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

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

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

(proj2 | (LSeg (|[a,c]|,|[a,d]|))) . |[a,c]| = |[a,c]| `2 by PSCOMP_1:23, RLTOPSP1:68

.= c by EUCLID:52 ;

hence c >= q by A4, A10, A11, FUNCT_2:35; :: thesis: verum

.= c by A5, A9, SEQ_4:44 ; :: thesis: verum

A13: W-bound (rectangle (a,b,c,d)) = a by A1, A2, Th36;

A14: upper_bound (proj2 | (LSeg (|[b,c]|,|[b,d]|))) = d

proof

A23:
E-most (rectangle (a,b,c,d)) = LSeg (|[b,c]|,|[b,d]|)
by A1, A2, Th45;
set X = LSeg (|[b,c]|,|[b,d]|);

reconsider Z = (proj2 | (LSeg (|[b,c]|,|[b,d]|))) .: the carrier of ((TOP-REAL 2) | (LSeg (|[b,c]|,|[b,d]|))) as Subset of REAL ;

A15: LSeg (|[b,c]|,|[b,d]|) = the carrier of ((TOP-REAL 2) | (LSeg (|[b,c]|,|[b,d]|))) by PRE_TOPC:8;

A16: for p being Real st p in Z holds

p <= d

p <= q ) holds

d <= q

.= d by A16, A20, SEQ_4:46 ; :: thesis: verum

end;reconsider Z = (proj2 | (LSeg (|[b,c]|,|[b,d]|))) .: the carrier of ((TOP-REAL 2) | (LSeg (|[b,c]|,|[b,d]|))) as Subset of REAL ;

A15: LSeg (|[b,c]|,|[b,d]|) = the carrier of ((TOP-REAL 2) | (LSeg (|[b,c]|,|[b,d]|))) by PRE_TOPC:8;

A16: for p being Real st p in Z holds

p <= d

proof

A20:
for q being Real st ( for p being Real st p in Z holds
let p be Real; :: thesis: ( p in Z implies p <= d )

assume p in Z ; :: thesis: p <= d

then consider p0 being object such that

A17: p0 in the carrier of ((TOP-REAL 2) | (LSeg (|[b,c]|,|[b,d]|))) and

p0 in the carrier of ((TOP-REAL 2) | (LSeg (|[b,c]|,|[b,d]|))) and

A18: p = (proj2 | (LSeg (|[b,c]|,|[b,d]|))) . p0 by FUNCT_2:64;

reconsider p0 = p0 as Point of (TOP-REAL 2) by A15, A17;

A19: |[b,c]| `2 = c by EUCLID:52;

|[b,d]| `2 = d by EUCLID:52;

then p0 `2 <= d by A2, A15, A17, A19, TOPREAL1:4;

hence p <= d by A15, A17, A18, PSCOMP_1:23; :: thesis: verum

end;assume p in Z ; :: thesis: p <= d

then consider p0 being object such that

A17: p0 in the carrier of ((TOP-REAL 2) | (LSeg (|[b,c]|,|[b,d]|))) and

p0 in the carrier of ((TOP-REAL 2) | (LSeg (|[b,c]|,|[b,d]|))) and

A18: p = (proj2 | (LSeg (|[b,c]|,|[b,d]|))) . p0 by FUNCT_2:64;

reconsider p0 = p0 as Point of (TOP-REAL 2) by A15, A17;

A19: |[b,c]| `2 = c by EUCLID:52;

|[b,d]| `2 = d by EUCLID:52;

then p0 `2 <= d by A2, A15, A17, A19, TOPREAL1:4;

hence p <= d by A15, A17, A18, PSCOMP_1:23; :: thesis: verum

p <= q ) holds

d <= q

proof

thus upper_bound (proj2 | (LSeg (|[b,c]|,|[b,d]|))) =
upper_bound Z
by PSCOMP_1:def 2
let q be Real; :: thesis: ( ( for p being Real st p in Z holds

p <= q ) implies d <= q )

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

p <= q ; :: thesis: d <= q

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

(proj2 | (LSeg (|[b,c]|,|[b,d]|))) . |[b,d]| = |[b,d]| `2 by PSCOMP_1:23, RLTOPSP1:68

.= d by EUCLID:52 ;

hence d <= q by A15, A21, A22, FUNCT_2:35; :: thesis: verum

end;p <= q ) implies d <= q )

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

p <= q ; :: thesis: d <= q

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

(proj2 | (LSeg (|[b,c]|,|[b,d]|))) . |[b,d]| = |[b,d]| `2 by PSCOMP_1:23, RLTOPSP1:68

.= d by EUCLID:52 ;

hence d <= q by A15, A21, A22, FUNCT_2:35; :: thesis: verum

.= d by A16, A20, SEQ_4:46 ; :: thesis: verum

E-bound (rectangle (a,b,c,d)) = b by A1, A2, Th38;

hence ( W-min (rectangle (a,b,c,d)) = |[a,c]| & E-max (rectangle (a,b,c,d)) = |[b,d]| ) by A3, A12, A13, A14, A23, PSCOMP_1:def 19, PSCOMP_1:def 23; :: thesis: verum