let C1 be non empty compact Subset of (TOP-REAL 2); :: thesis: for C2, S being non empty Subset of (TOP-REAL 2) st S = C1 \/ C2 & not proj1 .: C2 is empty & proj1 .: C2 is bounded_below holds
W-bound S = min (W-bound C1),(W-bound C2)
let C2, S be non empty Subset of (TOP-REAL 2); :: thesis: ( S = C1 \/ C2 & not proj1 .: C2 is empty & proj1 .: C2 is bounded_below implies W-bound S = min (W-bound C1),(W-bound C2) )
assume that
A1: S = C1 \/ C2 and
A2: ( not proj1 .: C2 is empty & proj1 .: C2 is bounded_below ) ; :: thesis: W-bound S = min (W-bound C1),(W-bound C2)
set P1 = proj1 .: C1;
set P2 = proj1 .: C2;
set PS = proj1 .: S;
A3: W-bound C1 = lower_bound (proj1 .: C1) by SPRECT_1:48;
A4: ( not proj1 .: C1 is empty & proj1 .: C1 is bounded_below ) ;
A5: W-bound C2 = lower_bound (proj1 .: C2) by SPRECT_1:48;
thus W-bound S = lower_bound (proj1 .: S) by SPRECT_1:48
.= lower_bound ((proj1 .: C1) \/ (proj1 .: C2)) by A1, RELAT_1:153
.= min (W-bound C1),(W-bound C2) by A2, A3, A5, A4, SPRECT_1:52 ; :: thesis: verum