theorem :: TEX_4:82

for Y being non empty TopStruct
for A being non empty Subset of Y holds Sspace A is SubSpace of MaxADSspace A