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

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