:: deftheorem defines L_Span EUCLID_7:def 9 :
for n being Nat
for X being Subset of (REAL n) holds L_Span X = meet { Y where Y is Subset of (REAL n) : ( Y is linear_manifold & X c= Y ) } ;