let Y be non empty TopStruct ; :: thesis: for Y0 being non proper SubSpace of Y holds TopStruct(# the carrier of Y0,the topology of Y0 #) = TopStruct(# the carrier of Y,the topology of Y #)
let Y0 be non proper SubSpace of Y; :: thesis: TopStruct(# the carrier of Y0,the topology of Y0 #) = TopStruct(# the carrier of Y,the topology of Y #)
consider A being Subset of Y such that
A1: A = the carrier of Y0 and
A2: not A is proper by Def3;
A3: the carrier of Y0 = the carrier of Y by A1, A2, SUBSET_1:def 7;
the topology of Y0 = the topology of Y

proof

now

let D be set ; :: thesis: ( D in the topology of Y0 implies D in the topology of Y )
assume A4: D in the topology of Y0 ; :: thesis: D in the topology of Y
then reconsider C = D as Subset of Y0 ;
consider E being Subset of Y such that
A5: E in the topology of Y and
A6: C = E /\ ([#] Y0) by A4, PRE_TOPC:def 9;
thus D in the topology of Y by A3, A5, A6, XBOOLE_1:28; :: thesis: verum

end;

then A7: the topology of Y0 c= the topology of Y by TARSKI:def 3;

now

let D be set ; :: thesis: ( D in the topology of Y implies D in the topology of Y0 )
assume A8: D in the topology of Y ; :: thesis: D in the topology of Y0
then reconsider E = D as Subset of Y ;
reconsider C = E as Subset of Y0 by A1, A2, SUBSET_1:def 7;

now

take E = E; :: thesis: ( E in the topology of Y & C = E /\ ([#] Y0) )
thus ( E in the topology of Y & C = E /\ ([#] Y0) ) by A8, XBOOLE_1:28; :: thesis: verum

end;

hence D in the topology of Y0 by PRE_TOPC:def 9; :: thesis: verum

end;

then the topology of Y c= the topology of Y0 by TARSKI:def 3;
hence the topology of Y0 = the topology of Y by A7, XBOOLE_0:def 10; :: thesis: verum

end;

hence TopStruct(# the carrier of Y0,the topology of Y0 #) = TopStruct(# the carrier of Y,the topology of Y #) by A1, A2, SUBSET_1:def 7; :: thesis: verum