:: deftheorem Def8 defines add-continuous RLTOPSP1:def 8 :
for X being non empty RLTopStruct holds
( X is add-continuous iff for x1, x2 being Point of X
for V being Subset of X st V is open & x1 + x2 in V holds
ex V1, V2 being Subset of X st
( V1 is open & V2 is open & x1 in V1 & x2 in V2 & V1 + V2 c= V ) );