let T1 be TopSpace; :: thesis: 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 ) )
let T2 be TopExtension of T1; :: thesis: 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 ) )
let A be Subset of T1; :: thesis: ( ( A is open implies A is open Subset of T2 ) & ( A is closed implies A is closed Subset of T2 ) )
A1: the carrier of T1 = the carrier of T2 by YELLOW_9:def 5;
reconsider B = A as Subset of T2 by YELLOW_9:def 5;
reconsider C = ([#] T2) \ B as Subset of T2 ;
A2: the topology of T1 c= the topology of T2 by YELLOW_9:def 5;
thus ( A is open implies A is open Subset of T2 ) :: thesis: ( A is closed implies A is closed Subset of T2 )

proof

assume A in the topology of T1 ; :: according to PRE_TOPC:def 2 :: thesis: A is open Subset of T2
then A in the topology of T2 by A2;
hence A is open Subset of T2 by PRE_TOPC:def 2; :: thesis: verum

end;

assume ([#] T1) \ A in the topology of T1 ; :: according to PRE_TOPC:def 2,PRE_TOPC:def 3 :: thesis: A is closed Subset of T2
then C is open by A2, A1;
hence A is closed Subset of T2 by PRE_TOPC:def 3; :: thesis: verum