consider F being Subset-Family of (Tunit_circle 2) such that
A1: F = {(CircleMap .: ].0,1.[),(CircleMap .: ].(1 / 2),(3 / 2).[)} and
A2: ( F is Cover of (Tunit_circle 2) & F is open ) and
A3: for U being Subset of (Tunit_circle 2) holds
( ( U = CircleMap .: ].0,1.[ implies ( union (IntIntervals (0,1)) = CircleMap " U & ( for d being Subset of R^1 st d in IntIntervals (0,1) holds
for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds
f is being_homeomorphism ) ) ) & ( U = CircleMap .: ].(1 / 2),(3 / 2).[ implies ( union (IntIntervals ((1 / 2),(3 / 2))) = CircleMap " U & ( for d being Subset of R^1 st d in IntIntervals ((1 / 2),(3 / 2)) holds
for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds
f is being_homeomorphism ) ) ) ) by TOPREALB:45;
take F ; :: thesis: ( F is Cover of (Tunit_circle 2) & F is open & ( for U being Subset of (Tunit_circle 2) st U in F holds
ex D being mutually-disjoint open Subset-Family of R^1 st
( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds
for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds
f is being_homeomorphism ) ) ) )
thus ( F is Cover of (Tunit_circle 2) & F is open ) by A2; :: thesis: for U being Subset of (Tunit_circle 2) st U in F holds
ex D being mutually-disjoint open Subset-Family of R^1 st
( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds
for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds
f is being_homeomorphism ) )
let U be Subset of (Tunit_circle 2); :: thesis: ( U in F implies ex D being mutually-disjoint open Subset-Family of R^1 st
( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds
for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds
f is being_homeomorphism ) ) )
assume A4: U in F ; :: thesis: ex D being mutually-disjoint open Subset-Family of R^1 st
( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds
for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds
f is being_homeomorphism ) )
per cases ( U = CircleMap .: ].0,1.[ or U = CircleMap .: ].(1 / 2),(3 / 2).[ ) by A1, A4, TARSKI:def 2;
suppose A5: U = CircleMap .: ].0,1.[ ; :: thesis: ex D being mutually-disjoint open Subset-Family of R^1 st
( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds
for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds
f is being_homeomorphism ) )
reconsider D = IntIntervals (0,1) as mutually-disjoint open Subset-Family of R^1 by Lm8, TOPREALB:4;
take D ; :: thesis: ( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds
for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds
f is being_homeomorphism ) )
thus ( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds
for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds
f is being_homeomorphism ) ) by A3, A5; :: thesis: verum
end;
suppose A6: U = CircleMap .: ].(1 / 2),(3 / 2).[ ; :: thesis: ex D being mutually-disjoint open Subset-Family of R^1 st
( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds
for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds
f is being_homeomorphism ) )
reconsider D = IntIntervals ((1 / 2),(3 / 2)) as mutually-disjoint open Subset-Family of R^1 by Lm9, TOPREALB:4;
take D ; :: thesis: ( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds
for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds
f is being_homeomorphism ) )
thus ( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds
for f being Function of (R^1 | d),((Tunit_circle 2) | U) st f = CircleMap | d holds
f is being_homeomorphism ) ) by A3, A6; :: thesis: verum
end;
end;