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 #)
A1: ex A being Subset of Y st
( A = the carrier of Y0 & not A is proper ) by Def1;
now :: thesis: for D being object st D in the topology of Y holds
D in the topology of Y0
let D be object ; :: thesis: ( D in the topology of Y implies D in the topology of Y0 )
assume A2: 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;
now :: thesis: ex E being Subset of Y st
( E in the topology of Y & C = E /\ ([#] Y0) )
take E = E; :: thesis: ( E in the topology of Y & C = E /\ ([#] Y0) )
thus ( E in the topology of Y & C = E /\ ([#] Y0) ) by A2, XBOOLE_1:28; :: thesis: verum
end;
hence D in the topology of Y0 by PRE_TOPC:def 4; :: thesis: verum
end;
then A3: the topology of Y c= the topology of Y0 by TARSKI:def 3;
A4: the carrier of Y0 = the carrier of Y by A1;
now :: thesis: for D being object st D in the topology of Y0 holds
D in the topology of Y
let D be object ; :: thesis: ( D in the topology of Y0 implies D in the topology of Y )
assume A5: D in the topology of Y0 ; :: thesis: D in the topology of Y
then reconsider C = D as Subset of Y0 ;
ex E being Subset of Y st
( E in the topology of Y & C = E /\ ([#] Y0) ) by A5, PRE_TOPC:def 4;
hence D in the topology of Y by A4, XBOOLE_1:28; :: thesis: verum
end;
then the topology of Y0 c= the topology of Y by TARSKI:def 3;
then the topology of Y0 = the topology of Y by A3;
hence TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y, the topology of Y #) by A1; :: thesis: verum