defpred S₁[ set ] means $1 in y=0-line ;
deffunc H₁( Element of (TOP-REAL 2)) -> set = { ((Ball |[($1 `1 ),r]|,r) \/ {$1}) where r is Element of REAL : r > 0 } ;
set X = y>=0-plane ;
deffunc H₂( Element of (TOP-REAL 2)) -> set = { ((Ball $1,r) /\ y>=0-plane ) where r is Element of REAL : r > 0 } ;
consider B being ManySortedSet of y>=0-plane 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 A2: S₁[z] ; :: thesis: not B . z is empty

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

end;

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

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

end;

end;

end;

then reconsider B = B as non-empty ManySortedSet of y>=0-plane ;
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 and
A6: 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 A7: z in w ; :: thesis: z in bool y>=0-plane

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

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

then consider r being Element of REAL such that
A8: z = (Ball |[(a `1 ),r]|,r) \/ {a} and
A9: r > 0 by A7;
Ball |[(a `1 ),r]|,r c= y>=0-plane by A9, Th24;
then z c= y>=0-plane by A8, 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 A7;
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;

A10: 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 A11: 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 A12: 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
A13: U = (Ball |[(y `1 ),r]|,r) \/ {y} and
A14: r > 0 by A12;
A15: ( x in Ball |[(y `1 ),r]|,r or x = y ) by A11, A13, SETWISEO:6;
then reconsider z = x as Element of (TOP-REAL 2) ;

now

set r2 = r - |.(z - |[(y `1 ),r]|).|;
assume A16: 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 )
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 A16, TOPREAL9:7;
then reconsider r1 = r, r2 = r - |.(z - |[(y `1 ),r]|).| as positive Real by XREAL_1:52;
A17: r2 > 0 ;
Ball |[(y `1 ),r]|,r misses y=0-line by A14, Th25;
then A18: not S₁[x] by A16, XBOOLE_0:3;
Ball |[(y `1 ),r]|,r c= y>=0-plane by A14, Th24;
then B . z = H<sub>2</sub>(z) by A16, A18, A1;
hence V in B . x by A17; :: thesis: V c= U
A19: Ball |[(y `1 ),r]|,r c= U by A13, XBOOLE_1:7;
r1 - r2 = |.(|[(y `1 ),r]| - z).| by TOPRNS_1:28;
then A20: Ball z,r2 c= Ball |[(y `1 ),r]|,r1 by Th26;
V c= Ball z,r2 by XBOOLE_1:17;
then V c= Ball |[(y `1 ),r]|,r1 by A20, XBOOLE_1:1;
hence V c= U by A19, XBOOLE_1:1; :: thesis: verum

end;

hence ex V being set st
( V in B . x & V c= U ) by A12, A15; :: 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
A21: U = (Ball y,r) /\ y>=0-plane and
r > 0 by A12;
reconsider z = x as Element of y>=0-plane by A11, A21, XBOOLE_0:def 4;
set r2 = r - |.(z - y).|;
z in Ball y,r by A11, A21, 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;
A22: z = |[(z `1 ),(z `2 )]| by EUCLID:57;

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

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

then z `2 = 0 by A22, Th19;
then |[(z `1 ),(r2 / 2)]| - z = |[((z `1 ) - (z `1 )),((r2 / 2) - 0 )]| by A22, EUCLID:66;
then |.(|[(z `1 ),(r2 / 2)]| - z).| = abs (r2 / 2) by TOPREAL6:31
.= r2 / 2 by ABSVALUE:def 1 ;
then |.(|[(z `1 ),(r2 / 2)]| - y).| <= (r2 / 2) + |.(z - y).| by TOPRNS_1:35;
then |.(y - |[(z `1 ),(r2 / 2)]|).| <= r - (r2 / 2) by TOPRNS_1:28;
then A24: Ball |[(z `1 ),(r2 / 2)]|,(r2 / 2) c= Ball y,r1 by Th26;
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 )
B . z = H₁(z) by A23, A1;
hence (Ball |[(z `1 ),(r2 / 2)]|,(r2 / 2)) \/ {z} in B . x ; :: thesis: (Ball |[(z `1 ),(r2 / 2)]|,(r2 / 2)) \/ {z} c= U
A25: {z} c= U by A11, ZFMISC_1:37;
Ball |[(z `1 ),(r2 / 2)]|,(r2 / 2) c= y>=0-plane by Th24;
then Ball |[(z `1 ),(r2 / 2)]|,(r2 / 2) c= U by A24, A21, XBOOLE_1:19;
hence (Ball |[(z `1 ),(r2 / 2)]|,(r2 / 2)) \/ {z} c= U by A25, XBOOLE_1:8; :: thesis: verum

end;

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

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

end;

end;

end;

end;

end;

A27: 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 that
A28: U1 in B . x and
A29: 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 A30: B . x = H₁(z) by A1;
then consider r1 being Real such that
A31: U1 = (Ball |[(z `1 ),r1]|,r1) \/ {z} and
A32: r1 > 0 by A28;
consider r2 being Real such that
A33: U2 = (Ball |[(z `1 ),r2]|,r2) \/ {z} and
A34: r2 > 0 by A29, A30;
( r1 <= r2 or r1 >= r2 ) ;
then consider U being set such that
A35: ( ( r1 <= r2 & U = U1 ) or ( r1 >= r2 & U = U2 ) ) ;
A36: U c= U2 by A31, A32, A33, A35, Th27, XBOOLE_1:9;
take U ; :: thesis: ( U in B . x & U c= U1 /\ U2 )
thus U in B . x by A28, A29, A35; :: thesis: U c= U1 /\ U2
U c= U1 by A31, A33, A34, A35, Th27, XBOOLE_1:9;
hence U c= U1 /\ U2 by A36, 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 A37: B . x = H₂(z) by A1;
then consider r1 being Real such that
A38: U1 = (Ball z,r1) /\ y>=0-plane and
r1 > 0 by A28;
consider r2 being Real such that
A39: U2 = (Ball z,r2) /\ y>=0-plane and
r2 > 0 by A29, A37;
( r1 <= r2 or r1 >= r2 ) ;
then consider U being set such that
A40: ( ( r1 <= r2 & U = U1 ) or ( r1 >= r2 & U = U2 ) ) ;
A41: U c= U2 by A38, A39, A40, JORDAN:18, XBOOLE_1:26;
take U ; :: thesis: ( U in B . x & U c= U1 /\ U2 )
thus U in B . x by A28, A29, A40; :: thesis: U c= U1 /\ U2
U c= U1 by A38, A39, A40, JORDAN:18, XBOOLE_1:26;
hence U c= U1 /\ U2 by A41, XBOOLE_1:19; :: thesis: verum

end;

end;

end;

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 A42: U in B . x ; :: thesis: x in U

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

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

A44: a in {a} by TARSKI:def 1;
ex r being Element of REAL st
( U = (Ball |[(a `1 ),r]|,r) \/ {a} & r > 0 ) by A43, A42;
hence x in U by A44, 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
A45: U = (Ball a,r) /\ y>=0-plane and
A46: r > 0 by A42;
a in Ball a,r by A46, Th17;
hence x in U by A45, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

then consider P being Subset-Family of y>=0-plane such that
P = Union B and
A47: for T being TopStruct st the carrier of T = y>=0-plane & the topology of T = UniCl P holds
( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds
B is Neighborhood_System of T9 ) ) by A27, A4, A10, 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 A47;
reconsider B = B as Neighborhood_System of T by A47;
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 }

defpred S₂[ Real] means $1 > 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 ]|};
A48: |[x,0 ]| in y>=0-plane ;
A49: for r being Real holds H₃(r) = H₄(r) by EUCLID:56;
A50: { H₃(r) where r is Real : S₂[r] } = { H₄(r) where r is Real : S₂[r] } from FRAENKEL:sch 5(A49);
S₁[|[x,0 ]|] ;
hence B . |[x,0 ]| = { ((Ball |[x,r]|,r) \/ {|[x,0 ]|}) where r is Element of REAL : r > 0 } by A48, A1, A50; :: 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 A51: y > 0 ; :: thesis: B . |[x,y]| = { ((Ball |[x,y]|,r) /\ y>=0-plane ) where r is Element of REAL : r > 0 }
then A52: |[x,y]| in y>=0-plane ;
not |[x,y]| in y=0-line by A51, Th19;
hence B . |[x,y]| = { ((Ball |[x,y]|,r) /\ y>=0-plane ) where r is Element of REAL : r > 0 } by A52, A1; :: thesis: verum