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