:: deftheorem Def18 defines MaxADSspace TEX_4:def 18 :
for Y being non empty TopStruct
for A being Subset of Y
for b₃ being strict SubSpace of Y holds
( b₃ = MaxADSspace A iff the carrier of b₃ = MaxADSet A );