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
S-bound S = min (S-bound C1),(S-bound C2)
let C1, C2 be non empty compact Subset of (TOP-REAL 2); :: thesis: ( S = C1 \/ C2 implies S-bound S = min (S-bound C1),(S-bound C2) )
assume A1: S = C1 \/ C2 ; :: thesis: S-bound S = min (S-bound C1),(S-bound C2)
A2: S-bound C1 = inf (proj2 .: C1) by Th49;
A3: ( not proj2 .: C2 is empty & proj2 .: C2 is bounded_below ) by Th46;
A4: ( not proj2 .: C1 is empty & proj2 .: C1 is bounded_below ) by Th46;
A5: S-bound C2 = inf (proj2 .: C2) by Th49;
thus S-bound S = inf (proj2 .: S) by Th49
.= inf ((proj2 .: C1) \/ (proj2 .: C2)) by A1, RELAT_1:153
.= min (S-bound C1),(S-bound C2) by A2, A5, A4, A3, Th52 ; :: thesis: verum