let X be RealNormSpace; :: thesis: for Y, Z being Subset of X st Z = the carrier of (Lin Y) holds
not Cl Z is empty
let Y, Z be Subset of X; :: thesis: ( Z = the carrier of (Lin Y) implies not Cl Z is empty )
assume A1: Z = the carrier of (Lin Y) ; :: thesis: not Cl Z is empty
Z c= Cl Z by PRETOPC18;
hence not Cl Z is empty by A1; :: thesis: verum