now :: thesis: for Y being Subset of REAL st Y is open holds
(f | X) " Y is open
let Y be Subset of REAL; :: thesis: ( Y is open implies (f | X) " Y is open )
assume Y is open ; :: thesis: (f | X) " Y is open
then A1: f " Y is open by Th8;
( the carrier of (T | X) = X & (f | X) " Y = X /\ (f " Y) ) by FUNCT_1:70, PRE_TOPC:8;
hence (f | X) " Y is open by A1, TSP_1:def 1; :: thesis: verum
end;
hence for b1 being RealMap of (T | X) st b1 = f | X holds
b1 is continuous by Th8; :: thesis: verum