Symbol CSubSp-->ClSubSp (#2865)
Symbol CSubSp-->ClSubSp (#2865)

* CSubSp-->ClSubSp

* comments: add precisions to definitions related to closed subspaces

* comments: add precision to definition of orthocomplement

* shorten hdmldef line

* comment of df-lvec

* slight rewording
metamath/set.mm,metamath/set.mm,metamath/set.mm