let T be non empty TopSpace; :: thesis: for f being Function of T,I[01] holds
( f is continuous iff for a, b being real number st 0 <= a & a < 1 & 0 < b & b <= 1 holds
( f " [.0 ,b.[ is open & f " ].a,1.] is open ) )
set A1 = { [.0 ,a.[ where a is Real : ( 0 < a & a <= 1 ) } ;
set A2 = { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } ;
set A3 = { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) } ;
reconsider B = ({ [.0 ,a.[ where a is Real : ( 0 < a & a <= 1 ) } \/ { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } ) \/ { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) } as Basis of I[01] by Th78;
let f be Function of T,I[01] ; :: thesis: ( f is continuous iff for a, b being real number st 0 <= a & a < 1 & 0 < b & b <= 1 holds
( f " [.0 ,b.[ is open & f " ].a,1.] is open ) )

hereby :: thesis: ( ( for a, b being real number st 0 <= a & a < 1 & 0 < b & b <= 1 holds
( f " [.0 ,b.[ is open & f " ].a,1.] is open ) ) implies f is continuous )

assume A1: f is continuous ; :: thesis: for a, b being real number st 0 <= a & a < 1 & 0 < b & b <= 1 holds
( f " [.0 ,b.[ is open & f " ].a,1.] is open )
let a, b be real number ; :: thesis: ( 0 <= a & a < 1 & 0 < b & b <= 1 implies ( f " [.0 ,b.[ is open & f " ].a,1.] is open ) )
reconsider x = a, y = b as Real by XREAL_0:def 1;
assume ( 0 <= a & a < 1 & 0 < b & b <= 1 ) ; :: thesis: ( f " [.0 ,b.[ is open & f " ].a,1.] is open )
then ( [.0 ,y.[ in { [.0 ,a.[ where a is Real : ( 0 < a & a <= 1 ) } & ].x,1.] in { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } ) ;
then ( [.0 ,y.[ in { [.0 ,a.[ where a is Real : ( 0 < a & a <= 1 ) } \/ { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } & ].x,1.] in { [.0 ,a.[ where a is Real : ( 0 < a & a <= 1 ) } \/ { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } ) by XBOOLE_0:def 3;
then ( [.0 ,y.[ in B & ].x,1.] in B ) by XBOOLE_0:def 3;
hence ( f " [.0 ,b.[ is open & f " ].a,1.] is open ) by A1, YELLOW_9:34; :: thesis: verum

end;

assume A2: for a, b being real number st 0 <= a & a < 1 & 0 < b & b <= 1 holds
( f " [.0 ,b.[ is open & f " ].a,1.] is open ) ; :: thesis: f is continuous

now

let A be Subset of I[01] ; :: thesis: ( A in B implies f " b₁ is open )
assume A in B ; :: thesis: f " b₁ is open
then A3: ( A in { [.0 ,a.[ where a is Real : ( 0 < a & a <= 1 ) } \/ { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } or A in { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) } ) by XBOOLE_0:def 3;

per cases ( A in { [.0 ,a.[ where a is Real : ( 0 < a & a <= 1 ) } or A in { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } or A in { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) } ) by A3, XBOOLE_0:def 3;

suppose A in { [.0 ,a.[ where a is Real : ( 0 < a & a <= 1 ) } ; :: thesis: f " b₁ is open

then ex a being Real st
( A = [.0 ,a.[ & 0 < a & a <= 1 ) ;
hence f " A is open by A2; :: thesis: verum

end;

suppose A in { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } ; :: thesis: f " b₁ is open

then ex a being Real st
( A = ].a,1.] & 0 <= a & a < 1 ) ;
hence f " A is open by A2; :: thesis: verum

end;

suppose A in { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) } ; :: thesis: f " b₁ is open

then consider a, b being Real such that
A4: ( A = ].a,b.[ & 0 <= a & a < b & b <= 1 ) ;
( 0 < b & a < 1 ) by A4, XXREAL_0:2;
then reconsider U = f " [.0 ,b.[, V = f " ].a,1.] as open Subset of T by A2, A4;
A = [.0 ,b.[ /\ ].a,1.] by A4, XXREAL_1:153;
then f " A = U /\ V by FUNCT_1:137;
hence f " A is open by TOPS_1:38; :: thesis: verum

end;

end;

end;

hence f is continuous by YELLOW_9:34; :: thesis: verum