let S be Subset of (TOP-REAL 2); 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); ( S = C1 \/ C2 implies E-bound S = max (E-bound C1),(E-bound C2) )
assume A1:
S = C1 \/ C2
; E-bound S = max (E-bound C1),(E-bound C2)
A2:
E-bound C1 = sup (proj1 .: C1)
by Th51;
A3:
( not proj1 .: C2 is empty & proj1 .: C2 is bounded_above )
by Th47;
A4:
( not proj1 .: C1 is empty & proj1 .: C1 is bounded_above )
by Th47;
A5:
E-bound C2 = sup (proj1 .: C2)
by Th51;
thus E-bound S =
sup (proj1 .: S)
by Th51
.=
sup ((proj1 .: C1) \/ (proj1 .: C2))
by A1, RELAT_1:153
.=
max (E-bound C1),(E-bound C2)
by A2, A5, A4, A3, Th53
; verum