let a, b, c, d be Real; ( 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
; ( 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
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
proof
let p be
Real;
( p in Z implies p >= c )
assume
p in Z
;
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;
verum
end;
A9:
for
q being
Real st ( for
p being
Real st
p in Z holds
p >= q ) holds
c >= q
proof
let q be
Real;
( ( 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
;
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;
verum
end;
thus lower_bound (proj2 | (LSeg (|[a,c]|,|[a,d]|))) =
lower_bound Z
by PSCOMP_1:def 1
.=
c
by A5, A9, SEQ_4:44
;
verum
end;
A12:
W-most (rectangle (a,b,c,d)) = LSeg (|[a,c]|,|[a,d]|)
by A1, A2, Th44;
A13:
W-bound (rectangle (a,b,c,d)) = a
by A1, A2, Th36;
A14:
upper_bound (proj2 | (LSeg (|[b,c]|,|[b,d]|))) = d
proof
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
proof
let p be
Real;
( p in Z implies p <= d )
assume
p in Z
;
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;
verum
end;
A20:
for
q being
Real st ( for
p being
Real st
p in Z holds
p <= q ) holds
d <= q
proof
let q be
Real;
( ( 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
;
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;
verum
end;
thus upper_bound (proj2 | (LSeg (|[b,c]|,|[b,d]|))) =
upper_bound Z
by PSCOMP_1:def 2
.=
d
by A16, A20, SEQ_4:46
;
verum
end;
A23:
E-most (rectangle (a,b,c,d)) = LSeg (|[b,c]|,|[b,d]|)
by A1, A2, Th45;
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; verum