Description: Real vector spaces are subcomplex vector spaces (elemental version). (Contributed by BJ, 6-Jan-2024)