set X = y>=0-plane ;
deffunc H₁( Element of (TOP-REAL 2)) -> set = { ((Ball |[($1 `1 ),r]|,r) \/ {$1}) where r is Element of REAL : r > 0 } ;
deffunc H₂( Element of (TOP-REAL 2)) -> set = { ((Ball $1,r) /\ y>=0-plane ) where r is Element of REAL : r > 0 } ;
defpred S₁[ set ] means $1 in y=0-line ;
consider B being ManySortedSet of such that
A1: for a being Element of y>=0-plane st a in y>=0-plane holds
( ( S₁[a] implies B . a = H₁(a) ) & ( not S₁[a] implies B . a = H₂(a) ) ) from PRE_CIRC:sch 2();
B is non-empty

proof

let z be set ; :: according to PBOOLE:def 16 :: thesis: ( not z in y>=0-plane or not B . z is empty )
assume z in y>=0-plane ; :: thesis: not B . z is empty
then reconsider s = z as Element of y>=0-plane ;

per cases ( S₁[z] or not S₁[z] ) ;

suppose S₁[z] ; :: thesis: not B . z is empty

then A2: B . s = H₁(s) by A1;
consider r being positive Element of REAL ;
set a = |[(s `1 ),r]|;
(Ball |[(s `1 ),r]|,r) \/ {s} in B . s by A2;
hence not B . z is empty ; :: thesis: verum

end;

suppose not S₁[z] ; :: thesis: not B . z is empty

then A3: B . s = H₂(s) by A1;
consider r being positive Element of REAL ;
(Ball s,r) /\ y>=0-plane in B . s by A3;
hence not B . z is empty ; :: thesis: verum

end;

end;

end;

then reconsider B = B as non-empty ManySortedSet of ;
A4: rng B c= bool (bool y>=0-plane )

proof

let w be set ; :: according to TARSKI:def 3 :: thesis: ( not w in rng B or w in bool (bool y>=0-plane ) )
assume w in rng B ; :: thesis: w in bool (bool y>=0-plane )
then consider a being set such that
A5: ( a in dom B & w = B . a ) by FUNCT_1:def 5;
reconsider a = a as Element of y>=0-plane by A5, PARTFUN1:def 4;
w c= bool y>=0-plane

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in w or z in bool y>=0-plane )
assume A6: z in w ; :: thesis: z in bool y>=0-plane

per cases ( w = H₁(a) or w = H₂(a) ) by A1, A5;

suppose w = H₁(a) ; :: thesis: z in bool y>=0-plane

then consider r being Element of REAL such that
A7: ( z = (Ball |[(a `1 ),r]|,r) \/ {a} & r > 0 ) by A6;
( Ball |[(a `1 ),r]|,r c= y>=0-plane & {a} c= y>=0-plane ) by A7, Th24;
then z c= y>=0-plane by A7, XBOOLE_1:8;
hence z in bool y>=0-plane ; :: thesis: verum

end;

suppose w = H₂(a) ; :: thesis: z in bool y>=0-plane

then ex r being Element of REAL st
( z = (Ball a,r) /\ y>=0-plane & r > 0 ) by A6;
then z c= y>=0-plane by XBOOLE_1:17;
hence z in bool y>=0-plane ; :: thesis: verum

end;

end;

end;

hence w in bool (bool y>=0-plane ) ; :: thesis: verum

end;

A8: for x, U being set st x in y>=0-plane & U in B . x holds
x in U

proof

let x, U be set ; :: thesis: ( x in y>=0-plane & U in B . x implies x in U )
assume x in y>=0-plane ; :: thesis: ( not U in B . x or x in U )
then reconsider a = x as Element of y>=0-plane ;
assume A9: U in B . x ; :: thesis: x in U

per cases ( B . x = H₁(a) or B . x = H₂(a) ) by A1;

suppose B . x = H₁(a) ; :: thesis: x in U

then consider r being Element of REAL such that
A10: ( U = (Ball |[(a `1 ),r]|,r) \/ {a} & r > 0 ) by A9;
a in {a} by TARSKI:def 1;
hence x in U by A10, XBOOLE_0:def 3; :: thesis: verum

end;

suppose B . x = H₂(a) ; :: thesis: x in U

then consider r being Element of REAL such that
A11: ( U = (Ball a,r) /\ y>=0-plane & r > 0 ) by A9;
a in Ball a,r by A11, Th17;
hence x in U by A11, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

A12: for x, y, U being set st x in U & U in B . y & y in y>=0-plane holds
ex V being set st
( V in B . x & V c= U )

proof

let x, y, U be set ; :: thesis: ( x in U & U in B . y & y in y>=0-plane implies ex V being set st
( V in B . x & V c= U ) )
assume A13: x in U ; :: thesis: ( not U in B . y or not y in y>=0-plane or ex V being set st
( V in B . x & V c= U ) )
assume A14: U in B . y ; :: thesis: ( not y in y>=0-plane or ex V being set st
( V in B . x & V c= U ) )
assume y in y>=0-plane ; :: thesis: ex V being set st
( V in B . x & V c= U )
then reconsider y = y as Element of y>=0-plane ;

per cases ( S₁[y] or not S₁[y] ) ;

suppose S₁[y] ; :: thesis: ex V being set st
( V in B . x & V c= U )

then B . y = H₁(y) by A1;
then consider r being Element of REAL such that
A15: ( U = (Ball |[(y `1 ),r]|,r) \/ {y} & r > 0 ) by A14;
A16: ( x in Ball |[(y `1 ),r]|,r or x = y ) by A13, A15, SETWISEO:6;
then reconsider z = x as Element of (TOP-REAL 2) ;

now

assume A17: x in Ball |[(y `1 ),r]|,r ; :: thesis: ex V being Element of bool the carrier of (TOP-REAL 2) st
( V in B . x & V c= U )
( Ball |[(y `1 ),r]|,r c= y>=0-plane & Ball |[(y `1 ),r]|,r misses y=0-line ) by A15, Th24, Th25;
then ( x in y>=0-plane & not S<sub>1</sub>[x] ) by A17, XBOOLE_0:3;
then A18: B . z = H<sub>2</sub>(z) by A1;
set r2 = r - |.(z - |[(y `1 ),r]|).|;
take V = (Ball z,(r - |.(z - |[(y `1 ),r]|).|)) /\ y>=0-plane ; :: thesis: ( V in B . x & V c= U )
|.(z - |[(y `1 ),r]|).| < r by A17, TOPREAL9:7;
then reconsider r1 = r, r2 = r - |.(z - |[(y `1 ),r]|).| as positive Real by XREAL_1:52;
r2 > 0 ;
hence V in B . x by A18; :: thesis: V c= U
r1 - r2 = |.(|[(y `1 ),r]| - z).| by TOPRNS_1:28;
then ( V c= Ball z,r2 & Ball z,r2 c= Ball |[(y `1 ),r]|,r1 ) by Th26, XBOOLE_1:17;
then ( V c= Ball |[(y `1 ),r]|,r1 & Ball |[(y `1 ),r]|,r c= U ) by A15, XBOOLE_1:1, XBOOLE_1:7;
hence V c= U by XBOOLE_1:1; :: thesis: verum

end;

hence ex V being set st
( V in B . x & V c= U ) by A14, A16; :: thesis: verum

end;

suppose not S₁[y] ; :: thesis: ex V being set st
( V in B . x & V c= U )

then B . y = H₂(y) by A1;
then consider r being Element of REAL such that
A19: ( U = (Ball y,r) /\ y>=0-plane & r > 0 ) by A14;
reconsider z = x as Element of y>=0-plane by A13, A19, XBOOLE_0:def 4;
set r2 = r - |.(z - y).|;
z in Ball y,r by A13, A19, XBOOLE_0:def 4;
then |.(z - y).| < r by TOPREAL9:7;
then reconsider r1 = r, r2 = r - |.(z - y).| as positive Real by XREAL_1:52;
A20: z = |[(z `1 ),(z `2 )]| by EUCLID:57;

per cases ( S₁[z] or not S₁[z] ) ;

suppose S₁[z] ; :: thesis: ex V being set st
( V in B . x & V c= U )

then A21: ( B . z = H₁(z) & z `2 = 0 ) by A1, A20, Th19;
set V = (Ball |[(z `1 ),(r2 / 2)]|,(r2 / 2)) \/ {z};
take (Ball |[(z `1 ),(r2 / 2)]|,(r2 / 2)) \/ {z} ; :: thesis: ( (Ball |[(z `1 ),(r2 / 2)]|,(r2 / 2)) \/ {z} in B . x & (Ball |[(z `1 ),(r2 / 2)]|,(r2 / 2)) \/ {z} c= U )
thus (Ball |[(z `1 ),(r2 / 2)]|,(r2 / 2)) \/ {z} in B . x by A21; :: thesis: (Ball |[(z `1 ),(r2 / 2)]|,(r2 / 2)) \/ {z} c= U
( |[(z `1 ),(r2 / 2)]| - z = |[((z `1 ) - (z `1 )),((r2 / 2) - 0 )]| & (z `1 ) - (z `1 ) = 0 ) by A20, A21, EUCLID:66;
then |.(|[(z `1 ),(r2 / 2)]| - z).| = abs (r2 / 2) by TOPREAL6:31
.= r2 / 2 by ABSVALUE:def 1 ;
then A22: |.(|[(z `1 ),(r2 / 2)]| - y).| <= (r2 / 2) + |.(z - y).| by TOPRNS_1:35;
then ( |.(|[(z `1 ),(r2 / 2)]| - y).| <= r - (r2 / 2) & r - (r2 / 2) < r ) by XREAL_1:46;
then |.(|[(z `1 ),(r2 / 2)]| - y).| < r by XXREAL_0:2;
then ( |[(z `1 ),(r2 / 2)]| in Ball y,r & |.(y - |[(z `1 ),(r2 / 2)]|).| <= r - (r2 / 2) ) by A22, TOPREAL9:7, TOPRNS_1:28;
then ( Ball |[(z `1 ),(r2 / 2)]|,(r2 / 2) c= y>=0-plane & Ball |[(z `1 ),(r2 / 2)]|,(r2 / 2) c= Ball y,r1 ) by Th24, Th26;
then ( Ball |[(z `1 ),(r2 / 2)]|,(r2 / 2) c= U & {z} c= U ) by A13, A19, XBOOLE_1:19, ZFMISC_1:37;
hence (Ball |[(z `1 ),(r2 / 2)]|,(r2 / 2)) \/ {z} c= U by XBOOLE_1:8; :: thesis: verum

end;

suppose not S₁[z] ; :: thesis: ex V being set st
( V in B . x & V c= U )

then A23: B . z = H₂(z) by A1;
take V = (Ball z,r2) /\ y>=0-plane ; :: thesis: ( V in B . x & V c= U )
thus V in B . x by A23; :: thesis: V c= U
|.(y - z).| = r1 - r2 by TOPRNS_1:28;
hence V c= U by A19, Th26, XBOOLE_1:26; :: thesis: verum

end;

end;

end;

end;

end;

for x, U1, U2 being set st x in y>=0-plane & U1 in B . x & U2 in B . x holds
ex U being set st
( U in B . x & U c= U1 /\ U2 )

proof

let x, U1, U2 be set ; :: thesis: ( x in y>=0-plane & U1 in B . x & U2 in B . x implies ex U being set st
( U in B . x & U c= U1 /\ U2 ) )
assume x in y>=0-plane ; :: thesis: ( not U1 in B . x or not U2 in B . x or ex U being set st
( U in B . x & U c= U1 /\ U2 ) )
then reconsider z = x as Element of y>=0-plane ;
assume A24: ( U1 in B . x & U2 in B . x ) ; :: thesis: ex U being set st
( U in B . x & U c= U1 /\ U2 )

per cases ( S₁[z] or not S₁[z] ) ;

suppose S₁[z] ; :: thesis: ex U being set st
( U in B . x & U c= U1 /\ U2 )

then A25: B . x = H₁(z) by A1;
then consider r1 being Real such that
A26: ( U1 = (Ball |[(z `1 ),r1]|,r1) \/ {z} & r1 > 0 ) by A24;
consider r2 being Real such that
A27: ( U2 = (Ball |[(z `1 ),r2]|,r2) \/ {z} & r2 > 0 ) by A24, A25;
( r1 <= r2 or r1 >= r2 ) ;
then consider U being set such that
A28: ( ( r1 <= r2 & U = U1 ) or ( r1 >= r2 & U = U2 ) ) ;
take U ; :: thesis: ( U in B . x & U c= U1 /\ U2 )
thus U in B . x by A24, A28; :: thesis: U c= U1 /\ U2
( U c= U1 & U c= U2 ) by A26, A27, A28, Th27, XBOOLE_1:9;
hence U c= U1 /\ U2 by XBOOLE_1:19; :: thesis: verum

end;

suppose not S₁[z] ; :: thesis: ex U being set st
( U in B . x & U c= U1 /\ U2 )

then A29: B . x = H₂(z) by A1;
then consider r1 being Real such that
A30: ( U1 = (Ball z,r1) /\ y>=0-plane & r1 > 0 ) by A24;
consider r2 being Real such that
A31: ( U2 = (Ball z,r2) /\ y>=0-plane & r2 > 0 ) by A24, A29;
( r1 <= r2 or r1 >= r2 ) ;
then consider U being set such that
A32: ( ( r1 <= r2 & U = U1 ) or ( r1 >= r2 & U = U2 ) ) ;
take U ; :: thesis: ( U in B . x & U c= U1 /\ U2 )
thus U in B . x by A24, A32; :: thesis: U c= U1 /\ U2
( U c= U1 & U c= U2 ) by A30, A31, A32, JORDAN:18, XBOOLE_1:26;
hence U c= U1 /\ U2 by XBOOLE_1:19; :: thesis: verum

end;

end;

end;

then consider P being Subset-Family of y>=0-plane such that
A33: ( P = Union B & ( for T being TopStruct st the carrier of T = y>=0-plane & the topology of T = UniCl P holds
( T is TopSpace & ( for T' being non empty TopSpace st T' = T holds
B is Neighborhood_System of T' ) ) ) ) by A4, A8, A12, TOPGEN_3:3;
set T = TopStruct(# y>=0-plane ,(UniCl P) #);
reconsider T = TopStruct(# y>=0-plane ,(UniCl P) #) as non empty strict TopSpace by A33;
reconsider B = B as Neighborhood_System of T by A33;
take T ; :: thesis: ( the carrier of T = y>=0-plane & ex B being Neighborhood_System of T st
( ( for x being Element of REAL holds B . |[x,0 ]| = { ((Ball |[x,r]|,r) \/ {|[x,0 ]|}) where r is Element of REAL : r > 0 } ) & ( for x, y being Element of REAL st y > 0 holds
B . |[x,y]| = { ((Ball |[x,y]|,r) /\ y>=0-plane ) where r is Element of REAL : r > 0 } ) ) )
thus the carrier of T = y>=0-plane ; :: thesis: ex B being Neighborhood_System of T st
( ( for x being Element of REAL holds B . |[x,0 ]| = { ((Ball |[x,r]|,r) \/ {|[x,0 ]|}) where r is Element of REAL : r > 0 } ) & ( for x, y being Element of REAL st y > 0 holds
B . |[x,y]| = { ((Ball |[x,y]|,r) /\ y>=0-plane ) where r is Element of REAL : r > 0 } ) )
take B ; :: thesis: ( ( for x being Element of REAL holds B . |[x,0 ]| = { ((Ball |[x,r]|,r) \/ {|[x,0 ]|}) where r is Element of REAL : r > 0 } ) & ( for x, y being Element of REAL st y > 0 holds
B . |[x,y]| = { ((Ball |[x,y]|,r) /\ y>=0-plane ) where r is Element of REAL : r > 0 } ) )

hereby :: thesis: for x, y being Element of REAL st y > 0 holds
B . |[x,y]| = { ((Ball |[x,y]|,r) /\ y>=0-plane ) where r is Element of REAL : r > 0 }

let x be Element of REAL ; :: thesis: B . |[x,0 ]| = { ((Ball |[x,r]|,r) \/ {|[x,0 ]|}) where r is Element of REAL : r > 0 }
deffunc H₃( Real) -> Element of bool the carrier of (TOP-REAL 2) = (Ball |[x,$1]|,$1) \/ {|[x,0 ]|};
deffunc H₄( Real) -> Element of bool the carrier of (TOP-REAL 2) = (Ball |[(|[x,0 ]| `1 ),$1]|,$1) \/ {|[x,0 ]|};
defpred S₂[ Real] means $1 > 0 ;
A34: for r being Real holds H₃(r) = H₄(r) by EUCLID:56;
A35: { H₃(r) where r is Real : S₂[r] } = { H₄(r) where r is Real : S₂[r] } from FRAENKEL:sch 5(A34);
( S₁[|[x,0 ]|] & |[x,0 ]| in y>=0-plane ) ;
hence B . |[x,0 ]| = { ((Ball |[x,r]|,r) \/ {|[x,0 ]|}) where r is Element of REAL : r > 0 } by A1, A35; :: thesis: verum

end;

let x, y be Element of REAL ; :: thesis: ( y > 0 implies B . |[x,y]| = { ((Ball |[x,y]|,r) /\ y>=0-plane ) where r is Element of REAL : r > 0 } )
assume y > 0 ; :: thesis: B . |[x,y]| = { ((Ball |[x,y]|,r) /\ y>=0-plane ) where r is Element of REAL : r > 0 }
then ( |[x,y]| in y>=0-plane & not |[x,y]| in y=0-line ) by Th19;
hence B . |[x,y]| = { ((Ball |[x,y]|,r) /\ y>=0-plane ) where r is Element of REAL : r > 0 } by A1; :: thesis: verum