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

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