X c= REAL n ;
then X c= [#] (REAL n) by SUBSET_1:def 3;
then [#] (REAL n) in { Y where Y is Subset of (REAL n) : ( Y is linear_manifold & X c= Y ) } ;
then reconsider Z = { Y where Y is Subset of (REAL n) : ( Y is linear_manifold & X c= Y ) } as non empty set ;
let x, y be Element of REAL n; :: according to EUCLID_7:def 8 :: thesis: for a, b being Element of REAL st x in L_Span X & y in L_Span X holds
(a * x) + (b * y) in L_Span X
let a, b be Element of REAL ; :: thesis: ( x in L_Span X & y in L_Span X implies (a * x) + (b * y) in L_Span X )
assume that
A1: x in L_Span X and
A2: y in L_Span X ; :: thesis: (a * x) + (b * y) in L_Span X
A3: for Y4 being set st Y4 in { Y where Y is Subset of (REAL n) : ( Y is linear_manifold & X c= Y ) } holds
(a * x) + (b * y) in Y4

proof

let Y4 be set ; :: thesis: ( Y4 in { Y where Y is Subset of (REAL n) : ( Y is linear_manifold & X c= Y ) } implies (a * x) + (b * y) in Y4 )
assume A4: Y4 in { Y where Y is Subset of (REAL n) : ( Y is linear_manifold & X c= Y ) } ; :: thesis: (a * x) + (b * y) in Y4
then A5: ex Y0 being Subset of (REAL n) st
( Y4 = Y0 & Y0 is linear_manifold & X c= Y0 ) ;
A6: y in Y4 by A2, A4, SETFAM_1:def 1;
x in Y4 by A1, A4, SETFAM_1:def 1;
hence (a * x) + (b * y) in Y4 by A6, A5; :: thesis: verum

end;

Z <> {} ;
hence (a * x) + (b * y) in L_Span X by A3, SETFAM_1:def 1; :: thesis: verum