for T1 being TopSpace
for T2 being TopExtension of T1
for A being Subset of T1 holds
( ( A is open implies A is open Subset of T2 ) & ( A is closed implies A is closed Subset of T2 ) )