for Y being non empty TopStruct
for Y0 being non empty SubSpace of Y
for Y1 being non empty V144() SubSpace of Y st Y0 is SubSpace of Y1 holds
Y0 is V144()