let Y be non empty TopStruct ; :: thesis: for x being Point of Y holds Sspace x is SubSpace of MaxADSspace x
let x be Point of Y; :: thesis: Sspace x is SubSpace of MaxADSspace x
( the carrier of (Sspace x) = {x} & the carrier of (MaxADSspace x) = MaxADSet x ) by Def17, TEX_2:def 4;
hence Sspace x is SubSpace of MaxADSspace x by Lm2, Th14; :: thesis: verum