let V be RealLinearSpace; :: thesis: for W being Subspace of V holds (0). V is Subspace of W
let W be Subspace of V; :: thesis: (0). V is Subspace of W
the carrier of ((0). V) = {(0. V)} by Def3
.= {(0. W)} by Def2 ;
hence (0). V is Subspace of W by Th28; :: thesis: verum