let a, b, c, d be real number ; ( 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:29;
A5:
for
p being
real number st
p in Z holds
p >= c
proof
let p be
real number ;
( p in Z implies p >= c )
assume
p in Z
;
p >= c
then consider p0 being
set 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:115;
reconsider p0 =
p0 as
Point of
(TOP-REAL 2) by A4, A6;
A8:
|[a,c]| `2 = c
by EUCLID:56;
|[a,d]| `2 = d
by EUCLID:56;
then
p0 `2 >= c
by A2, A4, A6, A8, TOPREAL1:10;
hence
p >= c
by A4, A6, A7, PSCOMP_1:70;
verum
end;
A9:
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 ;
( ( for p being real number st p in Z holds
p >= q ) implies c >= q )
assume A10:
for
p being
real number st
p in Z holds
p >= q
;
c >= q
A11:
|[a,c]| in LSeg |[a,c]|,
|[a,d]|
by RLTOPSP1:69;
(proj2 | (LSeg |[a,c]|,|[a,d]|)) . |[a,c]| =
|[a,c]| `2
by PSCOMP_1:70, RLTOPSP1:69
.=
c
by EUCLID:56
;
hence
c >= q
by A4, A10, A11, FUNCT_2:43;
verum
end;
thus lower_bound (proj2 | (LSeg |[a,c]|,|[a,d]|)) =
lower_bound Z
by PSCOMP_1:def 20
.=
c
by A5, A9, SEQ_4:61
;
verum
end;
A12:
W-most (rectangle a,b,c,d) = LSeg |[a,c]|,|[a,d]|
by A1, A2, Th54;
A13:
W-bound (rectangle a,b,c,d) = a
by A1, A2, Th46;
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:29;
A16:
for
p being
real number st
p in Z holds
p <= d
proof
let p be
real number ;
( p in Z implies p <= d )
assume
p in Z
;
p <= d
then consider p0 being
set 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:115;
reconsider p0 =
p0 as
Point of
(TOP-REAL 2) by A15, A17;
A19:
|[b,c]| `2 = c
by EUCLID:56;
|[b,d]| `2 = d
by EUCLID:56;
then
p0 `2 <= d
by A2, A15, A17, A19, TOPREAL1:10;
hence
p <= d
by A15, A17, A18, PSCOMP_1:70;
verum
end;
A20:
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 ;
( ( for p being real number st p in Z holds
p <= q ) implies d <= q )
assume A21:
for
p being
real number st
p in Z holds
p <= q
;
d <= q
A22:
|[b,d]| in LSeg |[b,c]|,
|[b,d]|
by RLTOPSP1:69;
(proj2 | (LSeg |[b,c]|,|[b,d]|)) . |[b,d]| =
|[b,d]| `2
by PSCOMP_1:70, RLTOPSP1:69
.=
d
by EUCLID:56
;
hence
d <= q
by A15, A21, A22, FUNCT_2:43;
verum
end;
thus upper_bound (proj2 | (LSeg |[b,c]|,|[b,d]|)) =
upper_bound Z
by PSCOMP_1:def 21
.=
d
by A16, A20, SEQ_4:63
;
verum
end;
A23:
E-most (rectangle a,b,c,d) = LSeg |[b,c]|,|[b,d]|
by A1, A2, Th55;
E-bound (rectangle a,b,c,d) = b
by A1, A2, Th48;
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 42, PSCOMP_1:def 46; verum