let V be RealUnitarySpace; :: 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 Def2
.= {(0. W)} by Def1 ;
hence (0). V is Subspace of W by Th22; :: thesis: verum