set A3 = { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) } ;
set A2 = { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } ;
set A1 = { [.0,a.[ where a is Real : ( 0 < a & a <= 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 Th74;
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 st 0 <= a & a < 1 & 0 < b & b <= 1 holds
( f " [.0,b.[ is open & f " ].a,1.] is open ) )
let f be Function of T,I[01]; :: thesis: ( f is continuous iff for a, b being Real 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 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 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; :: 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 ;
assume that
A2: 0 <= a and
A3: a < 1 and
A4: 0 < b and
A5: b <= 1 ; :: thesis: ( f " [.0,b.[ is open & f " ].a,1.] is open )
].x,1.] in { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } by A2, A3;
then ].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 A6: ].x,1.] in B by XBOOLE_0:def 3;
[.0,y.[ in { [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) } by A4, A5;
then [.0,y.[ 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 by XBOOLE_0:def 3;
hence ( f " [.0,b.[ is open & f " ].a,1.] is open ) by A6, A1, YELLOW_9:34; :: thesis: verum

end;

assume A7: for a, b being Real 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 :: thesis: for A being Subset of I[01] st A in B holds
f " A is open

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 A8: ( 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 A8, 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 A7; :: 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 A7; :: 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
A9: A = ].a,b.[ and
A10: 0 <= a and
A11: a < b and
A12: b <= 1 ;
a < 1 by A11, A12, XXREAL_0:2;
then reconsider U = f " [.0,b.[, V = f " ].a,1.] as open Subset of T by A10, A11, A7, A12;
A = [.0,b.[ /\ ].a,1.] by A9, A10, A12, XXREAL_1:153;
then f " A = U /\ V by FUNCT_1:68;
hence f " A is open ; :: thesis: verum

end;

end;

end;

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