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
proof
set X = LSeg (|[a,c]|,|[a,d]|);
reconsider Z = (proj2 | (LSeg (|[a,c]|,|[a,d]|))) .: the carrier of (() | (LSeg (|[a,c]|,|[a,d]|))) as Subset of REAL ;
A4: LSeg (|[a,c]|,|[a,d]|) = the carrier of (() | (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; :: 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 (() | (LSeg (|[a,c]|,|[a,d]|))) and
p0 in the carrier of (() | (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 () by A4, A6;
A8: |[a,c]| `2 = c by EUCLID:52;
|[a,d]| `2 = d by EUCLID:52;
then p0 `2 >= c by ;
hence p >= c by ; :: thesis: 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; :: 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
.= c by EUCLID:52 ;
hence c >= q by ; :: thesis: verum
end;
thus lower_bound (proj2 | (LSeg (|[a,c]|,|[a,d]|))) = lower_bound Z by PSCOMP_1:def 1
.= c by ; :: thesis: 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 (() | (LSeg (|[b,c]|,|[b,d]|))) as Subset of REAL ;
A15: LSeg (|[b,c]|,|[b,d]|) = the carrier of (() | (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; :: 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 (() | (LSeg (|[b,c]|,|[b,d]|))) and
p0 in the carrier of (() | (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 () by ;
A19: |[b,c]| `2 = c by EUCLID:52;
|[b,d]| `2 = d by EUCLID:52;
then p0 `2 <= d by ;
hence p <= d by ; :: thesis: 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; :: 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
.= d by EUCLID:52 ;
hence d <= q by ; :: thesis: verum
end;
thus upper_bound (proj2 | (LSeg (|[b,c]|,|[b,d]|))) = upper_bound Z by PSCOMP_1:def 2
.= d by ; :: thesis: 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 ; :: thesis: verum