consider F being Subset-Family of () such that
A1: F = {(),(CircleMap .: ].(1 / 2),(3 / 2).[)} and
A2: ( F is Cover of () & F is open ) and
A3: for U being Subset of () 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),(() | 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),(() | U) st f = CircleMap | d holds
f is being_homeomorphism ) ) ) ) by TOPREALB:45;
take F ; :: thesis: ( F is Cover of () & F is open & ( for U being Subset of () 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),(() | U) st f = CircleMap | d holds
f is being_homeomorphism ) ) ) )

thus ( F is Cover of () & F is open ) by A2; :: thesis: for U being Subset of () 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),(() | U) st f = CircleMap | d holds
f is being_homeomorphism ) )

let U be Subset of (); :: 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),(() | 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),(() | U) st f = CircleMap | d holds
f is being_homeomorphism ) )

per cases ( U = CircleMap .: ].0,1.[ or U = CircleMap .: ].(1 / 2),(3 / 2).[ ) by ;
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),(() | 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 ;
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),(() | 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),(() | 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),(() | 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 ;
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),(() | 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),(() | U) st f = CircleMap | d holds
f is being_homeomorphism ) ) by A3, A6; :: thesis: verum
end;
end;