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 Real holds B . |[x,0]| = { ((Ball (|[x,r]|,r)) \/ {|[x,0]|}) where r is Real : r > 0 } ) & ( for x, y being Real st y > 0 holds
B . |[x,y]| = { ((Ball (|[x,y]|,r)) /\ y>=0-plane) where r is Real : r > 0 } ) ) & the carrier of T2 = y>=0-plane & ex B being Neighborhood_System of T2 st
( ( for x being Real holds B . |[x,0]| = { ((Ball (|[x,r]|,r)) \/ {|[x,0]|}) where r is Real : r > 0 } ) & ( for x, y being Real st y > 0 holds
B . |[x,y]| = { ((Ball (|[x,y]|,r)) /\ y>=0-plane) where r is Real : r > 0 } ) ) implies T1 = T2 )
assume that
A56: the carrier of T1 = y>=0-plane and
A57: ex B being Neighborhood_System of T1 st
( ( for x being Real holds B . |[x,0]| = { ((Ball (|[x,r]|,r)) \/ {|[x,0]|}) where r is Real : r > 0 } ) & ( for x, y being Real st y > 0 holds
B . |[x,y]| = { ((Ball (|[x,y]|,r)) /\ y>=0-plane) where r is Real : r > 0 } ) ) and
A58: the carrier of T2 = y>=0-plane and
A59: ex B being Neighborhood_System of T2 st
( ( for x being Real holds B . |[x,0]| = { ((Ball (|[x,r]|,r)) \/ {|[x,0]|}) where r is Real : r > 0 } ) & ( for x, y being Real st y > 0 holds
B . |[x,y]| = { ((Ball (|[x,y]|,r)) /\ y>=0-plane) where r is Real : r > 0 } ) ) ; :: thesis: T1 = T2
consider B2 being Neighborhood_System of T2 such that
A60: for x being Real holds B2 . |[x,0]| = { ((Ball (|[x,r]|,r)) \/ {|[x,0]|}) where r is Real : r > 0 } and
A61: for x, y being Real st y > 0 holds
B2 . |[x,y]| = { ((Ball (|[x,y]|,r)) /\ y>=0-plane) where r is Real : r > 0 } by A59;
consider B1 being Neighborhood_System of T1 such that
A62: for x being Real holds B1 . |[x,0]| = { ((Ball (|[x,r]|,r)) \/ {|[x,0]|}) where r is Real : r > 0 } and
A63: for x, y being Real st y > 0 holds
B1 . |[x,y]| = { ((Ball (|[x,y]|,r)) /\ y>=0-plane) where r is Real : r > 0 } by A57;
now :: thesis: for a being object st a in y>=0-plane holds
B1 . a = B2 . a
let a be object ; :: 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 ;
A64: z = |[(z `1),(z `2)]| by EUCLID:53;
then ( z `2 = 0 or z `2 > 0 ) by Th18;
then ( ( z `2 = 0 & B1 . z = { ((Ball (|[(z `1),r]|,r)) \/ {|[(z `1),0]|}) where r is Real : r > 0 } & B2 . z = { ((Ball (|[(z `1),r]|,r)) \/ {|[(z `1),0]|}) where r is Real : r > 0 } ) or ( z `2 > 0 & B1 . z = { ((Ball (|[(z `1),(z `2)]|,r)) /\ y>=0-plane) where r is Real : r > 0 } & B2 . z = { ((Ball (|[(z `1),(z `2)]|,r)) /\ y>=0-plane) where r is Real : r > 0 } ) ) by A62, A63, A60, A61, A64;
hence B1 . a = B2 . a ; :: thesis: verum
end;
hence T1 = T2 by A56, A58, Th24, PBOOLE:3; :: thesis: verum