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 ;
hence A is open by Th95; :: thesis: verum
end;
hence X0 is open SubSpace of X by TSEP_1:def 1; :: thesis: verum
end;