set f = + (x,r);
consider BB being Neighborhood_System of Niemytzki-plane such that
A1: for x being Real holds BB . |[x,0]| = { ((Ball (|[x,q]|,q)) \/ {|[x,0]|}) where q is Real : q > 0 } and
A2: for x, y being Real st y > 0 holds
BB . |[x,y]| = { ((Ball (|[x,y]|,q)) /\ y>=0-plane) where q is Real : q > 0 } by Def3;
A3: dom BB = y>=0-plane by Lm1, PARTFUN1:def 2;
now :: thesis: for a, b being Real st 0 <= a & a < 1 & 0 < b & b <= 1 holds
( (+ (x,r)) " [.0,b.[ is open & (+ (x,r)) " ].a,1.] is open )
let a, b be Real; :: thesis: ( 0 <= a & a < 1 & 0 < b & b <= 1 implies ( (+ (x,r)) " [.0,b.[ is open & (+ (x,r)) " ].a,1.] is open ) )
assume that
A4: 0 <= a and
A5: a < 1 and
A6: 0 < b and
A7: b <= 1 ; :: thesis: ( (+ (x,r)) " [.0,b.[ is open & (+ (x,r)) " ].a,1.] is open )
now :: thesis: for c being Element of Niemytzki-plane st c in (+ (x,r)) " [.0,b.[ holds
ex U being Subset of Niemytzki-plane st
( U in Union BB & c in U & U c= (+ (x,r)) " [.0,b.[ )
let c be Element of Niemytzki-plane; :: thesis: ( c in (+ (x,r)) " [.0,b.[ implies ex U being Subset of Niemytzki-plane st
( b2 in Union BB & U in b2 & b2 c= (+ (x,r)) " [.0,b.[ ) )
assume c in (+ (x,r)) " [.0,b.[ ; :: thesis: ex U being Subset of Niemytzki-plane st
( b2 in Union BB & U in b2 & b2 c= (+ (x,r)) " [.0,b.[ )
then A8: (+ (x,r)) . c in [.0,b.[ by FUNCT_1:def 7;
c in y>=0-plane by Lm1;
then reconsider z = c as Point of (TOP-REAL 2) ;
z = |[(z `1),(z `2)]| by EUCLID:53;
then A9: z `2 >= 0 by Lm1, Th18;
per cases ( (+ (x,r)) . c = 0 or ( 0 < (+ (x,r)) . c & (+ (x,r)) . c < b ) ) by A8, XXREAL_1:3;
suppose A10: (+ (x,r)) . c = 0 ; :: thesis: ex U being Subset of Niemytzki-plane st
( b2 in Union BB & U in b2 & b2 c= (+ (x,r)) " [.0,b.[ )
reconsider r1 = r * b as positive Real by A6;
reconsider U = (Ball (|[x,r1]|,r1)) \/ {|[x,0]|} as Subset of Niemytzki-plane by Th27;
take U = U; :: thesis: ( U in Union BB & c in U & U c= (+ (x,r)) " [.0,b.[ )
A11: |[x,0]| in y>=0-plane ;
U in { ((Ball (|[x,q]|,q)) \/ {|[x,0]|}) where q is Real : q > 0 } ;
then A12: U in BB . |[x,0]| by A1;
z = |[x,0]| by A10, A9, Th60;
hence ( U in Union BB & c in U & U c= (+ (x,r)) " [.0,b.[ ) by A12, A11, A3, A6, Th67, CARD_5:2, ZFMISC_1:136; :: thesis: verum
end;
suppose A13: ( 0 < (+ (x,r)) . c & (+ (x,r)) . c < b ) ; :: thesis: ex U being Subset of Niemytzki-plane st
( b2 in Union BB & U in b2 & b2 c= (+ (x,r)) " [.0,b.[ )
reconsider r1 = r * b as positive Real by A6;
reconsider U = Ball (|[x,r1]|,r1) as Subset of Niemytzki-plane by Th29;
take U = U; :: thesis: ( U in Union BB & c in U & U c= (+ (x,r)) " [.0,b.[ )
A14: |[x,r1]| in y>=0-plane ;
U c= y>=0-plane by Th20;
then U /\ y>=0-plane = U by XBOOLE_1:28;
then U in { ((Ball (|[x,r1]|,q)) /\ y>=0-plane) where q is Real : q > 0 } ;
then U in BB . |[x,r1]| by A2;
hence U in Union BB by A14, A3, CARD_5:2; :: thesis: ( c in U & U c= (+ (x,r)) " [.0,b.[ )
A15: (+ (x,r)) " ].0,b.[ c= (+ (x,r)) " [.0,b.[ by RELAT_1:143, XXREAL_1:45;
Ball (|[x,(r * b)]|,(r * b)) c= (+ (x,r)) " ].0,b.[ by A13, Th66;
hence ( c in U & U c= (+ (x,r)) " [.0,b.[ ) by A15, A13, A7, A9, Th68; :: thesis: verum
end;
end;
end;
hence (+ (x,r)) " [.0,b.[ is open by YELLOW_9:31; :: thesis: (+ (x,r)) " ].a,1.] is open
now :: thesis: for c being Element of Niemytzki-plane st c in (+ (x,r)) " ].a,1.] holds
ex U being Subset of Niemytzki-plane st
( U in Union BB & c in U & U c= (+ (x,r)) " ].a,1.] )
let c be Element of Niemytzki-plane; :: thesis: ( c in (+ (x,r)) " ].a,1.] implies ex U being Subset of Niemytzki-plane st
( b2 in Union BB & U in b2 & b2 c= (+ (x,r)) " ].a,1.] ) )
c in y>=0-plane by Lm1;
then reconsider z = c as Point of (TOP-REAL 2) ;
assume c in (+ (x,r)) " ].a,1.] ; :: thesis: ex U being Subset of Niemytzki-plane st
( b2 in Union BB & U in b2 & b2 c= (+ (x,r)) " ].a,1.] )
then A16: (+ (x,r)) . c in ].a,1.] by FUNCT_1:def 7;
then A17: (+ (x,r)) . c > a by XXREAL_1:2;
A18: (+ (x,r)) . c <= 1 by A16, XXREAL_1:2;
A19: z = |[(z `1),(z `2)]| by EUCLID:53;
then A20: z `2 >= 0 by Lm1, Th18;
per cases ( z `2 > 0 or ( (+ (x,r)) . c = 1 & z `2 = 0 ) or ( a < (+ (x,r)) . c & (+ (x,r)) . c < 1 ) ) by A19, A16, A18, Lm1, Th18, XXREAL_0:1, XXREAL_1:2;
suppose z `2 > 0 ; :: thesis: ex U being Subset of Niemytzki-plane st
( b2 in Union BB & U in b2 & b2 c= (+ (x,r)) " ].a,1.] )
then consider r1 being positive Real such that
A21: r1 <= z `2 and
A22: Ball (z,r1) c= (+ (x,r)) " ].a,1.] by A4, A17, Th69;
reconsider U = Ball (z,r1) as Subset of Niemytzki-plane by A19, A21, Th29;
U c= y>=0-plane by A19, A21, Th20;
then A23: U /\ y>=0-plane = U by XBOOLE_1:28;
U in { ((Ball (|[(z `1),(z `2)]|,q)) /\ y>=0-plane) where q is Real : q > 0 } by A23, A19;
then A24: U in BB . |[(z `1),(z `2)]| by A21, A2;
take U = U; :: thesis: ( U in Union BB & c in U & U c= (+ (x,r)) " ].a,1.] )
|[(z `1),(z `2)]| in y>=0-plane by A21;
hence U in Union BB by A24, A3, CARD_5:2; :: thesis: ( c in U & U c= (+ (x,r)) " ].a,1.] )
thus ( c in U & U c= (+ (x,r)) " ].a,1.] ) by A22, Th13; :: thesis: verum
end;
suppose A25: ( (+ (x,r)) . c = 1 & z `2 = 0 ) ; :: thesis: ex U being Subset of Niemytzki-plane st
( b2 in Union BB & U in b2 & b2 c= (+ (x,r)) " ].a,1.] )
then consider r1 being positive Real such that
A26: (Ball (|[(z `1),r1]|,r1)) \/ {z} c= (+ (x,r)) " {1} by Th70;
reconsider U = (Ball (|[(z `1),r1]|,r1)) \/ {z} as Subset of Niemytzki-plane by A19, A25, Th27;
U in { ((Ball (|[(z `1),q]|,q)) \/ {|[(z `1),0]|}) where q is Real : q > 0 } by A19, A25;
then A27: U in BB . |[(z `1),(z `2)]| by A1, A25;
take U = U; :: thesis: ( U in Union BB & c in U & U c= (+ (x,r)) " ].a,1.] )
|[(z `1),(z `2)]| in y>=0-plane by A25;
hence U in Union BB by A27, A3, CARD_5:2; :: thesis: ( c in U & U c= (+ (x,r)) " ].a,1.] )
thus c in U by ZFMISC_1:136; :: thesis: U c= (+ (x,r)) " ].a,1.]
1 in ].a,1.] by A5, XXREAL_1:2;
then {1} c= ].a,1.] by ZFMISC_1:31;
then (+ (x,r)) " {1} c= (+ (x,r)) " ].a,1.] by RELAT_1:143;
hence U c= (+ (x,r)) " ].a,1.] by A26; :: thesis: verum
end;
suppose ( a < (+ (x,r)) . c & (+ (x,r)) . c < 1 ) ; :: thesis: ex U being Subset of Niemytzki-plane st
( b2 in Union BB & U in b2 & b2 c= (+ (x,r)) " ].a,1.] )
then (+ (x,r)) . c in ].a,1.[ by XXREAL_1:4;
then consider r1 being positive Real such that
A28: r1 <= z `2 and
A29: Ball (z,r1) c= (+ (x,r)) " ].a,1.[ by A4, A20, Th65;
reconsider U = Ball (z,r1) as Subset of Niemytzki-plane by A19, A28, Th29;
U c= y>=0-plane by A19, A28, Th20;
then A30: U /\ y>=0-plane = U by XBOOLE_1:28;
U in { ((Ball (|[(z `1),(z `2)]|,q)) /\ y>=0-plane) where q is Real : q > 0 } by A30, A19;
then A31: U in BB . |[(z `1),(z `2)]| by A28, A2;
take U = U; :: thesis: ( U in Union BB & c in U & U c= (+ (x,r)) " ].a,1.] )
|[(z `1),(z `2)]| in y>=0-plane by A28;
hence U in Union BB by A31, A3, CARD_5:2; :: thesis: ( c in U & U c= (+ (x,r)) " ].a,1.] )
(+ (x,r)) " ].a,1.[ c= (+ (x,r)) " ].a,1.] by RELAT_1:143, XXREAL_1:41;
hence ( c in U & U c= (+ (x,r)) " ].a,1.] ) by A29, Th13; :: thesis: verum
end;
end;
end;
hence (+ (x,r)) " ].a,1.] is open by YELLOW_9:31; :: thesis: verum
end;
hence + (x,r) is continuous by Th75; :: thesis: verum