let a, b, c, d be Real; :: thesis: ( a <= b & c <= d implies W-bound (rectangle (a,b,c,d)) = a )
assume that
A1: a <= b and
A2: c <= d ; :: thesis: W-bound (rectangle (a,b,c,d)) = a
set X = rectangle (a,b,c,d);
reconsider Z = (proj1 | (rectangle (a,b,c,d))) .: the carrier of (() | (rectangle (a,b,c,d))) as Subset of REAL ;
A3: rectangle (a,b,c,d) = the carrier of (() | (rectangle (a,b,c,d))) by PRE_TOPC:8;
A4: for p being Real st p in Z holds
p >= a
proof
let p be Real; :: thesis: ( p in Z implies p >= a )
assume p in Z ; :: thesis: p >= a
then consider p0 being object such that
A5: p0 in the carrier of (() | (rectangle (a,b,c,d))) and
p0 in the carrier of (() | (rectangle (a,b,c,d))) and
A6: p = (proj1 | (rectangle (a,b,c,d))) . p0 by FUNCT_2:64;
reconsider p0 = p0 as Point of () by A3, A5;
rectangle (a,b,c,d) = { q where q is Point of () : ( ( q `1 = a & q `2 <= d & q `2 >= c ) or ( q `1 <= b & q `1 >= a & q `2 = d ) or ( q `1 <= b & q `1 >= a & q `2 = c ) or ( q `1 = b & q `2 <= d & q `2 >= c ) ) } by ;
then ex q being Point of () st
( p0 = q & ( ( q `1 = a & q `2 <= d & q `2 >= c ) or ( q `1 <= b & q `1 >= a & q `2 = d ) or ( q `1 <= b & q `1 >= a & q `2 = c ) or ( q `1 = b & q `2 <= d & q `2 >= c ) ) ) by A3, A5;
hence p >= a by ; :: thesis: verum
end;
A7: for q being Real st ( for p being Real st p in Z holds
p >= q ) holds
a >= q
proof
let q be Real; :: thesis: ( ( for p being Real st p in Z holds
p >= q ) implies a >= q )

assume A8: for p being Real st p in Z holds
p >= q ; :: thesis: a >= q
|[a,c]| in LSeg (|[a,c]|,|[b,c]|) by RLTOPSP1:68;
then A9: |[a,c]| in (LSeg (|[a,c]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[b,d]|)) by XBOOLE_0:def 3;
rectangle (a,b,c,d) = ((LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|))) \/ ((LSeg (|[a,c]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[b,d]|))) by SPPOL_2:def 3;
then A10: |[a,c]| in rectangle (a,b,c,d) by ;
then (proj1 | (rectangle (a,b,c,d))) . |[a,c]| = |[a,c]| `1 by PSCOMP_1:22
.= a by EUCLID:52 ;
hence a >= q by ; :: thesis: verum
end;
thus W-bound (rectangle (a,b,c,d)) = lower_bound (proj1 | (rectangle (a,b,c,d))) by PSCOMP_1:def 7
.= lower_bound Z by PSCOMP_1:def 1
.= a by ; :: thesis: verum