let Y be TopStruct ; :: thesis: for Y0 being SubSpace of Y
for A being Subset of Y st A = the carrier of Y0 holds
( A is proper iff Y0 is proper )
let Y0 be SubSpace of Y; :: thesis: for A being Subset of Y st A = the carrier of Y0 holds
( A is proper iff Y0 is proper )
let A be Subset of Y; :: thesis: ( A = the carrier of Y0 implies ( A is proper iff Y0 is proper ) )
assume A1: A = the carrier of Y0 ; :: thesis: ( A is proper iff Y0 is proper )

hereby :: thesis: ( Y0 is proper implies A is proper )

assume A is proper ; :: thesis: Y0 is proper
then for A being Subset of Y st A = the carrier of Y0 holds
A is proper by A1;
hence Y0 is proper by Def3; :: thesis: verum

end;

thus ( Y0 is proper implies A is proper ) by A1, Def3; :: thesis: verum