thus id T is open :: thesis: id T is continuous

proof

let A be Subset of T; :: according to T_0TOPSP:def 2 :: thesis: ( not A is open or (id T) .: A is open )
assume A is open ; :: thesis: (id T) .: A is open
hence (id T) .: A is open by FUNCT_1:92; :: thesis: verum

end;

let V be Subset of T; :: according to PRE_TOPC:def 6 :: thesis: ( not V is closed or (id T) " V is closed )
assume V is closed ; :: thesis: (id T) " V is closed
hence (id T) " V is closed by FUNCT_2:94; :: thesis: verum