the carrier of (Pre-Lp-Space (M,k)) = CosetSet (M,k) by Def11;
hence not Pre-Lp-Space (M,k) is empty ; :: thesis: verum