**Description:** A closed subspace is a subspace. (Contributed by NM, 19-Oct-1999)
(New usage is discouraged.)

Ref | Expression | ||
---|---|---|---|

Hypothesis | chshi.1 | $${\u22a2}{H}\in {\mathbf{C}}_{\mathscr{H}}$$ | |

Assertion | chshii | $${\u22a2}{H}\in {\mathbf{S}}_{\mathscr{H}}$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | chshi.1 | $${\u22a2}{H}\in {\mathbf{C}}_{\mathscr{H}}$$ | |

2 | chsh | $${\u22a2}{H}\in {\mathbf{C}}_{\mathscr{H}}\to {H}\in {\mathbf{S}}_{\mathscr{H}}$$ | |

3 | 1 2 | ax-mp | $${\u22a2}{H}\in {\mathbf{S}}_{\mathscr{H}}$$ |