:: deftheorem defines linear_manifold EUCLID_7:def 8 :
for n being Nat
for X being Subset of (REAL n) holds
( X is linear_manifold iff for x, y being Element of REAL n
for a, b being Element of REAL st x in X & y in X holds
(a * x) + (b * y) in X );