let Y be TopStruct ; :: thesis: for Y0 being SubSpace of Y st the carrier of Y0 = the carrier of Y holds
not Y0 is proper
let Y0 be SubSpace of Y; :: thesis: ( the carrier of Y0 = the carrier of Y implies not Y0 is proper )
reconsider A = the carrier of Y0 as Subset of Y by Lm1;
assume A1: the carrier of Y0 = the carrier of Y ; :: thesis: not Y0 is proper
now :: thesis: ex A being Subset of Y st
( A = the carrier of Y0 & not A is proper )
take A = A; :: thesis: ( A = the carrier of Y0 & not A is proper )
thus ( A = the carrier of Y0 & not A is proper ) by A1; :: thesis: verum
end;
hence not Y0 is proper ; :: thesis: verum