let V be RealNormSpace; :: thesis: for W being SubRealNormSpace of V holds W is Subspace of V
let W be SubRealNormSpace of V; :: thesis: W is Subspace of V
( the carrier of W c= the carrier of V & 0. W = 0. V & the addF of W = the addF of V || the carrier of W & the Mult of W = the Mult of V | [:REAL, the carrier of W:] & the normF of W = the normF of V | the carrier of W ) by DUALSP01:def 16;
hence W is Subspace of V by RLSUB_1:def 2; :: thesis: verum