let X be non empty TopSpace; :: thesis: for X0 being non empty SubSpace of X holds

( X0 is open SubSpace of X iff TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to X0 )

let X0 be non empty SubSpace of X; :: thesis: ( X0 is open SubSpace of X iff TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to X0 )

thus ( X0 is open SubSpace of X implies TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to X0 ) :: thesis: ( TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to X0 implies X0 is open SubSpace of X )

( X0 is open SubSpace of X iff TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to X0 )

let X0 be non empty SubSpace of X; :: thesis: ( X0 is open SubSpace of X iff TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to X0 )

thus ( X0 is open SubSpace of X implies TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to X0 ) :: thesis: ( TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to X0 implies X0 is open SubSpace of X )

proof

thus
( TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to X0 implies X0 is open SubSpace of X )
:: thesis: verum
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;

assume X0 is open SubSpace of X ; :: thesis: TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to X0

then A is open by TSEP_1:def 1;

then TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to A by Th95;

hence TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to X0 by Def10; :: thesis: verum

end;assume X0 is open SubSpace of X ; :: thesis: TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to X0

then A is open by TSEP_1:def 1;

then TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to A by Th95;

hence TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to X0 by Def10; :: thesis: verum

proof

assume A1:
TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to X0
; :: thesis: X0 is open SubSpace of X

end;now :: thesis: for A being Subset of X st A = the carrier of X0 holds

A is open

hence
X0 is open SubSpace of X
by TSEP_1:def 1; :: thesis: verumA is open

let A be Subset of X; :: thesis: ( A = the carrier of X0 implies A is open )

assume A = the carrier of X0 ; :: thesis: A is open

then TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to A by A1, Def10;

hence A is open by Th95; :: thesis: verum

end;assume A = the carrier of X0 ; :: thesis: A is open

then TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to A by A1, Def10;

hence A is open by Th95; :: thesis: verum