let S be Subset of (TOP-REAL 2); :: thesis: for C1, C2 being non empty compact Subset of (TOP-REAL 2) st S = C1 \/ C2 holds
E-bound S = max ((E-bound C1),(E-bound C2))
let C1, C2 be non empty compact Subset of (TOP-REAL 2); :: thesis: ( S = C1 \/ C2 implies E-bound S = max ((E-bound C1),(E-bound C2)) )
assume A1: S = C1 \/ C2 ; :: thesis: E-bound S = max ((E-bound C1),(E-bound C2))
A2: E-bound C1 = upper_bound (proj1 .: C1) by Th51;
A3: ( not proj1 .: C2 is empty & proj1 .: C2 is bounded_above ) ;
A5: E-bound C2 = upper_bound (proj1 .: C2) by Th51;
thus E-bound S = upper_bound (proj1 .: S) by Th51
.= upper_bound ((proj1 .: C1) \/ (proj1 .: C2)) by A1, RELAT_1:120
.= max ((E-bound C1),(E-bound C2)) by A2, A5, A3, SEQ_4:143 ; :: thesis: verum