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 )

then C is open by A2, A1;

hence A is closed Subset of T2 by PRE_TOPC:def 3; :: thesis: verum

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
([#] T1) \ A in the topology of T1
; :: according to PRE_TOPC:def 2,PRE_TOPC:def 3 :: thesis: A is closed Subset of T2
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;then A in the topology of T2 by A2;

hence A is open Subset of T2 by PRE_TOPC:def 2; :: thesis: verum

then C is open by A2, A1;

hence A is closed Subset of T2 by PRE_TOPC:def 3; :: thesis: verum