let T1, T2 be non empty strict TopSpace; :: thesis: ( the carrier of T1 = y>=0-plane & ex B being Neighborhood_System of T1 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 } ) ) & the carrier of T2 = y>=0-plane & ex B being Neighborhood_System of T2 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 } ) ) implies T1 = T2 )
assume that
A53: the carrier of T1 = y>=0-plane and
A54: ex B being Neighborhood_System of T1 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 } ) ) and
A55: the carrier of T2 = y>=0-plane and
A56: ex B being Neighborhood_System of T2 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 } ) ) ; :: thesis: T1 = T2
consider B2 being Neighborhood_System of T2 such that
A57: for x being Element of REAL holds B2 . |[x,0]| = { ((Ball (|[x,r]|,r)) \/ {|[x,0]|}) where r is Element of REAL : r > 0 } and
A58: for x, y being Element of REAL st y > 0 holds
B2 . |[x,y]| = { ((Ball (|[x,y]|,r)) /\ y>=0-plane) where r is Element of REAL : r > 0 } by A56;
consider B1 being Neighborhood_System of T1 such that
A59: for x being Element of REAL holds B1 . |[x,0]| = { ((Ball (|[x,r]|,r)) \/ {|[x,0]|}) where r is Element of REAL : r > 0 } and
A60: for x, y being Element of REAL st y > 0 holds
B1 . |[x,y]| = { ((Ball (|[x,y]|,r)) /\ y>=0-plane) where r is Element of REAL : r > 0 } by A54;

now

let a be set ; :: thesis: ( a in y>=0-plane implies B1 . a = B2 . a )
assume a in y>=0-plane ; :: thesis: B1 . a = B2 . a
then reconsider z = a as Element of y>=0-plane ;
A61: z = |[(z `1),(z `2)]| by EUCLID:53;
then ( z `2 = 0 or z `2 > 0 ) by Th22;
then ( ( z `2 = 0 & B1 . z = { ((Ball (|[(z `1),r]|,r)) \/ {|[(z `1),0]|}) where r is Element of REAL : r > 0 } & B2 . z = { ((Ball (|[(z `1),r]|,r)) \/ {|[(z `1),0]|}) where r is Element of REAL : r > 0 } ) or ( z `2 > 0 & B1 . z = { ((Ball (|[(z `1),(z `2)]|,r)) /\ y>=0-plane) where r is Element of REAL : r > 0 } & B2 . z = { ((Ball (|[(z `1),(z `2)]|,r)) /\ y>=0-plane) where r is Element of REAL : r > 0 } ) ) by A59, A60, A57, A58, A61;
hence B1 . a = B2 . a ; :: thesis: verum

end;

hence T1 = T2 by A53, A55, Th28, PBOOLE:3; :: thesis: verum