reconsider O = 0. (TOP-REAL 2) as Point of (Euclid 2) by EUCLID:67;
let sn be Real; for p2 being Point of (TOP-REAL 2) st - 1 < sn & sn < 1 holds
ex K being non empty compact Subset of (TOP-REAL 2) st
( K = (sn -FanMorphW) .: K & ex V2 being Subset of (TOP-REAL 2) st
( p2 in V2 & V2 is open & V2 c= K & (sn -FanMorphW) . p2 in V2 ) )
let p2 be Point of (TOP-REAL 2); ( - 1 < sn & sn < 1 implies ex K being non empty compact Subset of (TOP-REAL 2) st
( K = (sn -FanMorphW) .: K & ex V2 being Subset of (TOP-REAL 2) st
( p2 in V2 & V2 is open & V2 c= K & (sn -FanMorphW) . p2 in V2 ) ) )
A1:
TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2)
by EUCLID:def 8;
TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2)
by EUCLID:def 8;
then reconsider V0 = Ball (O,(|.p2.| + 1)) as Subset of (TOP-REAL 2) ;
( O in V0 & V0 c= cl_Ball (O,(|.p2.| + 1)) )
by GOBOARD6:1, METRIC_1:14;
then reconsider K0 = cl_Ball (O,(|.p2.| + 1)) as non empty compact Subset of (TOP-REAL 2) by A1, Th15;
set q3 = (sn -FanMorphW) . p2;
reconsider VV0 = V0 as Subset of (TopSpaceMetr (Euclid 2)) ;
reconsider u2 = p2 as Point of (Euclid 2) by EUCLID:67;
reconsider u3 = (sn -FanMorphW) . p2 as Point of (Euclid 2) by EUCLID:67;
A2:
(sn -FanMorphW) .: K0 c= K0
VV0 is open
by TOPMETR:14;
then A8:
V0 is open
by Lm11, PRE_TOPC:30;
A9:
|.p2.| < |.p2.| + 1
by XREAL_1:29;
then
|.(- p2).| < |.p2.| + 1
by TOPRNS_1:26;
then
|.((0. (TOP-REAL 2)) - p2).| < |.p2.| + 1
by RLVECT_1:4;
then
dist (O,u2) < |.p2.| + 1
by JGRAPH_1:28;
then A10:
p2 in V0
by METRIC_1:11;
|.((sn -FanMorphW) . p2).| = |.p2.|
by Th33;
then
|.(- ((sn -FanMorphW) . p2)).| < |.p2.| + 1
by A9, TOPRNS_1:26;
then
|.((0. (TOP-REAL 2)) - ((sn -FanMorphW) . p2)).| < |.p2.| + 1
by RLVECT_1:4;
then
dist (O,u3) < |.p2.| + 1
by JGRAPH_1:28;
then A11:
(sn -FanMorphW) . p2 in V0
by METRIC_1:11;
assume A12:
( - 1 < sn & sn < 1 )
; ex K being non empty compact Subset of (TOP-REAL 2) st
( K = (sn -FanMorphW) .: K & ex V2 being Subset of (TOP-REAL 2) st
( p2 in V2 & V2 is open & V2 c= K & (sn -FanMorphW) . p2 in V2 ) )
K0 c= (sn -FanMorphW) .: K0
then
K0 = (sn -FanMorphW) .: K0
by A2, XBOOLE_0:def 10;
hence
ex K being non empty compact Subset of (TOP-REAL 2) st
( K = (sn -FanMorphW) .: K & ex V2 being Subset of (TOP-REAL 2) st
( p2 in V2 & V2 is open & V2 c= K & (sn -FanMorphW) . p2 in V2 ) )
by A10, A8, A11, METRIC_1:14; verum