defpred S₁[ object ] means $1 in y=0-line ;
deffunc H₁( Element of (TOP-REAL 2)) -> set = { ((Ball (|[($1 `1),r]|,r)) \/ {$1}) where r is 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 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

let z be object ; :: according to PBOOLE:def 13 :: thesis:
assume z in y>=0-plane ; :: thesis:
then reconsider s = z as Element of y>=0-plane ;

suppose A2: S₁[z] ; :: thesis:

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

end;

suppose A3: not S₁[z] ; :: thesis:

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

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 object ; :: according to TARSKI:def 3 :: thesis:
reconsider ww = w as set by TARSKI:1;
assume w in rng B ; :: thesis:
then consider a being object such that
A5: a in dom B and
A6: w = B . a by FUNCT_1:def 3;
reconsider a = a as Element of y>=0-plane by A5;
ww c= bool y>=0-plane

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
reconsider zz = z as set by TARSKI:1;
assume A7: z in ww ; :: thesis:

per cases by A1, A6;

suppose w = H₁(a) ; :: thesis:

then consider r being 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, Th20;
then zz c= y>=0-plane by A8, XBOOLE_1:8;
hence z in bool y>=0-plane ; :: thesis:

end;

suppose w = H₂(a) ; :: thesis:

then ex r being Real st
( z = (Ball (a,r)) /\ y>=0-plane & r > 0 ) by A7;
then zz c= y>=0-plane by XBOOLE_1:17;
hence z in bool y>=0-plane ; :: thesis:

end;

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

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:
assume A11: x in U ; :: thesis:
assume A12: U in B . y ; :: thesis:
assume y in y>=0-plane ; :: thesis:
then reconsider y = y as Element of y>=0-plane ;

per cases ;

suppose S₁[y] ; :: thesis:

then B . y = H₁(y) by A1;
then consider r being 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, ZFMISC_1:136;
then reconsider z = x as Element of (TOP-REAL 2) ;

now :: thesis:

set r2 = r - |.(z - |[(y `1),r]|).|;
assume A16: x in Ball (|[(y `1),r]|,r) ; :: thesis:
take V = (Ball (z,(r - |.(z - |[(y `1),r]|).|))) /\ y>=0-plane; :: thesis:
|.(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:50;
A17: r2 > 0 ;
Ball (|[(y `1),r]|,r) misses y=0-line by A14, Th21;
then A18: not S₁[x] by A16, XBOOLE_0:3;
Ball (|[(y `1),r]|,r) c= y>=0-plane by A14, Th20;
then B . z = H₂(z) by A16, A18, A1;
hence V in B . x by A17; :: thesis:
A19: Ball (|[(y `1),r]|,r) c= U by A13, XBOOLE_1:7;
r1 - r2 = |.(|[(y `1),r]| - z).| by TOPRNS_1:27;
then A20: Ball (z,r2) c= Ball (|[(y `1),r]|,r1) by Th22;
V c= Ball (z,r2) by XBOOLE_1:17;
then V c= Ball (|[(y `1),r]|,r1) by A20;
hence V c= U by A19; :: thesis:

end;

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

end;

suppose not S₁[y] ; :: thesis:

then B . y = H₂(y) by A1;
then consider r being 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:50;
A22: z = |[(z `1),(z `2)]| by EUCLID:53;

per cases ;

suppose A23: S₁[z] ; :: thesis:

then z `2 = 0 by A22, Th15;
then |[(z `1),(r2 / 2)]| - z = |[((z `1) - (z `1)),((r2 / 2) - 0)]| by A22, EUCLID:62;
then |.(|[(z `1),(r2 / 2)]| - z).| = |.(r2 / 2).| by TOPREAL6:23
.= r2 / 2 by ABSVALUE:def 1 ;
then |.(|[(z `1),(r2 / 2)]| - y).| <= (r2 / 2) + |.(z - y).| by TOPRNS_1:34;
then |.(y - |[(z `1),(r2 / 2)]|).| <= r - (r2 / 2) by TOPRNS_1:27;
then A24: Ball (|[(z `1),(r2 / 2)]|,(r2 / 2)) c= Ball (y,r1) by Th22;
set V = (Ball (|[(z `1),(r2 / 2)]|,(r2 / 2))) \/ {z};
take (Ball (|[(z `1),(r2 / 2)]|,(r2 / 2))) \/ {z} ; :: thesis:
B . z = H₁(z) by A23, A1;
hence (Ball (|[(z `1),(r2 / 2)]|,(r2 / 2))) \/ {z} in B . x ; :: thesis:
A25: {z} c= U by A11, ZFMISC_1:31;
Ball (|[(z `1),(r2 / 2)]|,(r2 / 2)) c= y>=0-plane by Th20;
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:

end;

suppose A26: not S₁[z] ; :: thesis:

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

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:
assume x in y>=0-plane ; :: thesis:
then reconsider z = x as Element of y>=0-plane ;
assume that
A28: U1 in B . x and
A29: U2 in B . x ; :: thesis:

per cases ;

suppose S₁[z] ; :: thesis:

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, Th23, XBOOLE_1:9;
take U ; :: thesis:
thus U in B . x by A28, A29, A35; :: thesis:
U c= U1 by A31, A33, A34, A35, Th23, XBOOLE_1:9;
hence U c= U1 /\ U2 by A36, XBOOLE_1:19; :: thesis:

end;

suppose not S₁[z] ; :: thesis:

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:
thus U in B . x by A28, A29, A40; :: thesis:
U c= U1 by A38, A39, A40, JORDAN:18, XBOOLE_1:26;
hence U c= U1 /\ U2 by A41, XBOOLE_1:19; :: thesis:

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:
assume x in y>=0-plane ; :: thesis:
then reconsider a = x as Element of y>=0-plane ;
assume A42: U in B . x ; :: thesis:

per cases by A1;

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

A44: a in {a} by TARSKI:def 1;
ex r being 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:

end;

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

then consider r being Real such that
A45: U = (Ball (a,r)) /\ y>=0-plane and
A46: r > 0 by A42;
a in Ball (a,r) by A46, Th13;
hence x in U by A45, XBOOLE_0:def 4; :: thesis:

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:
thus the carrier of T = y>=0-plane ; :: thesis:
take B ; :: thesis:

hereby :: thesis:

defpred S₂[ Real] means $1 > 0 ;
let x be Real; :: thesis:
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:52;
A50: { H₄(r) where r is Real : S₂[r] } c= { H₃(r1) where r1 is Real : S₂[r1] }

proof

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume e in { H₄(r) where r is Real : S₂[r] } ; :: thesis:
then consider r being Real such that
A51: ( e = H₄(r) & S₂[r] ) ;
( e = H₃(r) & S₂[r] ) by A49, A51;
hence e in { H₃(r1) where r1 is Real : S₂[r1] } ; :: thesis:

end;

{ H₃(r) where r is Real : S₂[r] } c= { H₄(r1) where r1 is Real : S₂[r1] }

proof

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume e in { H₃(r) where r is Real : S₂[r] } ; :: thesis:
then consider r being Real such that
A52: ( e = H₃(r) & S₂[r] ) ;
( e = H₄(r) & S₂[r] ) by A49, A52;
hence e in { H₄(r1) where r1 is Real : S₂[r1] } ; :: thesis:

end;

then A53: { H₃(r) where r is Real : S₂[r] } = { H₄(r) where r is Real : S₂[r] } by A50;
S₁[|[x,0]|] ;
then B . |[x,0]| = H₁(|[x,0]|) by A48, A1;
hence B . |[x,0]| = { ((Ball (|[x,r]|,r)) \/ {|[x,0]|}) where r is Real : r > 0 } by A53; :: thesis:

end;

let x, y be Real; :: thesis:
assume A54: y > 0 ; :: thesis:
then A55: |[x,y]| in y>=0-plane ;
not |[x,y]| in y=0-line by A54, Th15;
hence B . |[x,y]| = { ((Ball (|[x,y]|,r)) /\ y>=0-plane) where r is Real : r > 0 } by A55, A1; :: thesis: