let a, b, c, d be real number ; :: thesis: ( a <= b & c <= d implies W-bound (closed_inside_of_rectangle a,b,c,d) = a )
assume A1:
( a <= b & c <= d )
; :: thesis: W-bound (closed_inside_of_rectangle a,b,c,d) = a
set X = closed_inside_of_rectangle a,b,c,d;
reconsider Z = (proj1 | (closed_inside_of_rectangle a,b,c,d)) .: the carrier of ((TOP-REAL 2) | (closed_inside_of_rectangle a,b,c,d)) as Subset of REAL ;
A2:
closed_inside_of_rectangle a,b,c,d = the carrier of ((TOP-REAL 2) | (closed_inside_of_rectangle a,b,c,d))
by PRE_TOPC:29;
A3:
|[a,c]| in closed_inside_of_rectangle a,b,c,d
by A1, TOPREALA:52;
A4:
for p being real number st p in Z holds
p >= a
proof
let p be
real number ;
:: thesis: ( p in Z implies p >= a )
assume
p in Z
;
:: thesis: p >= a
then consider p0 being
set such that A5:
p0 in the
carrier of
((TOP-REAL 2) | (closed_inside_of_rectangle a,b,c,d))
and
p0 in the
carrier of
((TOP-REAL 2) | (closed_inside_of_rectangle a,b,c,d))
and A6:
p = (proj1 | (closed_inside_of_rectangle a,b,c,d)) . p0
by FUNCT_2:115;
ex
p1 being
Point of
(TOP-REAL 2) st
(
p0 = p1 &
a <= p1 `1 &
p1 `1 <= b &
c <= p1 `2 &
p1 `2 <= d )
by A2, A5;
hence
p >= a
by A2, A5, A6, PSCOMP_1:69;
:: thesis: verum
end;
A7:
for q being real number st ( for p being real number st p in Z holds
p >= q ) holds
a >= q
proof
let q be
real number ;
:: thesis: ( ( for p being real number st p in Z holds
p >= q ) implies a >= q )
assume A8:
for
p being
real number st
p in Z holds
p >= q
;
:: thesis: a >= q
A9:
(
|[a,c]| `1 = a &
|[a,c]| `2 = c )
by EUCLID:56;
(proj1 | (closed_inside_of_rectangle a,b,c,d)) . |[a,c]| = |[a,c]| `1
by A1, PSCOMP_1:69, TOPREALA:52;
hence
a >= q
by A2, A3, A8, A9, FUNCT_2:43;
:: thesis: verum
end;
not Z is empty
by A3;
hence
W-bound (closed_inside_of_rectangle a,b,c,d) = a
by A4, A7, SEQ_4:61; :: thesis: verum