let X be non empty TopSpace; :: thesis: for A being Subset of X st A <> the carrier of X & A is dense holds
not X modified_with_respect_to A is almost_discrete
let A be Subset of X; :: thesis: ( A <> the carrier of X & A is dense implies not X modified_with_respect_to A is almost_discrete )
assume A1: A <> the carrier of X ; :: thesis: ( not A is dense or not X modified_with_respect_to A is almost_discrete )
set Z = X modified_with_respect_to A;
assume A2: A is dense ; :: thesis: not X modified_with_respect_to A is almost_discrete
now :: thesis: ex C being Subset of (X modified_with_respect_to A) st
( C <> the carrier of (X modified_with_respect_to A) & C is everywhere_dense )
reconsider C = A as Subset of (X modified_with_respect_to A) by TMAP_1:93;
take C = C; :: thesis: ( C <> the carrier of (X modified_with_respect_to A) & C is everywhere_dense )
thus ( C <> the carrier of (X modified_with_respect_to A) & C is everywhere_dense ) by A1, A2, Th5, TMAP_1:93; :: thesis: verum
end;
hence not X modified_with_respect_to A is almost_discrete by Th32; :: thesis: verum