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

proof

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

end;

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