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 )

proof

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;

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

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

now :: thesis: for A being Subset of X st A = the carrier of X0 holds
A 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;

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

end;