let X be TopSpace; :: thesis: for X1, X2 being TopSpace st X2 = TopStruct(# the carrier of X1, the topology of X1 #) holds

( X1 is open SubSpace of X iff X2 is open SubSpace of X )

let X1, X2 be TopSpace; :: thesis: ( X2 = TopStruct(# the carrier of X1, the topology of X1 #) implies ( X1 is open SubSpace of X iff X2 is open SubSpace of X ) )

assume A1: X2 = TopStruct(# the carrier of X1, the topology of X1 #) ; :: thesis: ( X1 is open SubSpace of X iff X2 is open SubSpace of X )

thus ( X1 is open SubSpace of X implies X2 is open SubSpace of X ) :: thesis: ( X2 is open SubSpace of X implies X1 is open SubSpace of X )

then reconsider Y1 = X1 as SubSpace of X by A1, Th7;

reconsider A1 = the carrier of Y1 as Subset of X by TSEP_1:1;

A1 is open by A1, A3, TSEP_1:16;

hence X1 is open SubSpace of X by TSEP_1:16; :: thesis: verum

( X1 is open SubSpace of X iff X2 is open SubSpace of X )

let X1, X2 be TopSpace; :: thesis: ( X2 = TopStruct(# the carrier of X1, the topology of X1 #) implies ( X1 is open SubSpace of X iff X2 is open SubSpace of X ) )

assume A1: X2 = TopStruct(# the carrier of X1, the topology of X1 #) ; :: thesis: ( X1 is open SubSpace of X iff X2 is open SubSpace of X )

thus ( X1 is open SubSpace of X implies X2 is open SubSpace of X ) :: thesis: ( X2 is open SubSpace of X implies X1 is open SubSpace of X )

proof

assume A3:
X2 is open SubSpace of X
; :: thesis: X1 is open SubSpace of X
assume A2:
X1 is open SubSpace of X
; :: thesis: X2 is open SubSpace of X

then reconsider Y2 = X2 as SubSpace of X by A1, Th7;

reconsider A2 = the carrier of Y2 as Subset of X by TSEP_1:1;

A2 is open by A1, A2, TSEP_1:16;

hence X2 is open SubSpace of X by TSEP_1:16; :: thesis: verum

end;then reconsider Y2 = X2 as SubSpace of X by A1, Th7;

reconsider A2 = the carrier of Y2 as Subset of X by TSEP_1:1;

A2 is open by A1, A2, TSEP_1:16;

hence X2 is open SubSpace of X by TSEP_1:16; :: thesis: verum

then reconsider Y1 = X1 as SubSpace of X by A1, Th7;

reconsider A1 = the carrier of Y1 as Subset of X by TSEP_1:1;

A1 is open by A1, A3, TSEP_1:16;

hence X1 is open SubSpace of X by TSEP_1:16; :: thesis: verum