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
A1: the carrier of (Sspace x) = {x} by TEX_2:def 2;
the carrier of (MaxADSspace x) = MaxADSet x by Def17;
hence Sspace x is SubSpace of MaxADSspace x by A1, Lm2, Th12; :: thesis: verum