set X = { l where l is Linear_Combination of A : verum } ;
{ l where l is Linear_Combination of A : verum } c= the carrier of (LC_RLSpace V)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { l where l is Linear_Combination of A : verum } or x in the carrier of (LC_RLSpace V) )
assume x in { l where l is Linear_Combination of A : verum } ; :: thesis: x in the carrier of (LC_RLSpace V)
then ex l being Linear_Combination of A st x = l ;
hence x in the carrier of (LC_RLSpace V) by Def16; :: thesis: verum

end;

then reconsider X = { l where l is Linear_Combination of A : verum } as Subset of (LC_RLSpace V) ;
ZeroLC V is Linear_Combination of A by Th34;
then A1: ZeroLC V in X ;
X is linearly-closed

proof

thus for v, u being VECTOR of (LC_RLSpace V) st v in X & u in X holds
v + u in X :: according to RLSUB_1:def 1 :: thesis: for b₁ being Element of REAL
for b₂ being Element of the carrier of (LC_RLSpace V) holds
( not b₂ in X or b₁ * b₂ in X )

proof

let v, u be VECTOR of (LC_RLSpace V); :: thesis: ( v in X & u in X implies v + u in X )
assume that
A2: v in X and
A3: u in X ; :: thesis: v + u in X
consider l1 being Linear_Combination of A such that
A4: v = l1 by A2;
consider l2 being Linear_Combination of A such that
A5: u = l2 by A3;
( v = vector (LC_RLSpace V),l1 & u = vector (LC_RLSpace V),l2 ) by A4, A5, Def1, RLVECT_1:3;
then v + u = l1 + l2 by Th96;
then v + u is Linear_Combination of A by Th59;
hence v + u in X ; :: thesis: verum

end;

let a be Real; :: thesis: for b₁ being Element of the carrier of (LC_RLSpace V) holds
( not b₁ in X or a * b₁ in X )
let v be VECTOR of (LC_RLSpace V); :: thesis: ( not v in X or a * v in X )
assume v in X ; :: thesis: a * v in X
then consider l being Linear_Combination of A such that
A6: v = l ;
a * v = a * (vector (LC_RLSpace V),l) by A6, Def1, RLVECT_1:3
.= a * l by Th97 ;
then a * v is Linear_Combination of A by Th67;
hence a * v in X ; :: thesis: verum

end;

hence ex b₁ being strict Subspace of LC_RLSpace V st the carrier of b₁ = { l where l is Linear_Combination of A : verum } by A1, RLSUB_1:43; :: thesis: verum