let Y be TopStruct ; :: thesis: for Y0, Y1 being SubSpace of Y st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & Y0 is proper holds
Y1 is proper
let Y0, Y1 be SubSpace of Y; :: thesis: ( TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & Y0 is proper implies Y1 is proper )
assume A1: TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) ; :: thesis: ( not Y0 is proper or Y1 is proper )
assume Y0 is proper ; :: thesis: Y1 is proper
then for A being Subset of Y st A = the carrier of Y1 holds
A is proper by A1, Def3;
hence Y1 is proper by Def3; :: thesis: verum