let V be RealLinearSpace; :: thesis: for W being Subspace of V holds
( Up W is Affine & 0. V in the carrier of W )
let W be Subspace of V; :: thesis: ( Up W is Affine & 0. V in the carrier of W )
for x, y being VECTOR of V
for a being Real st x in Up W & y in Up W holds
((1 - a) * x) + (a * y) in Up W

proof

let x, y be VECTOR of V; :: thesis: for a being Real st x in Up W & y in Up W holds
((1 - a) * x) + (a * y) in Up W
let a be Real; :: thesis: ( x in Up W & y in Up W implies ((1 - a) * x) + (a * y) in Up W )
assume ( x in Up W & y in Up W ) ; :: thesis: ((1 - a) * x) + (a * y) in Up W
then ( x in W & y in W ) by STRUCT_0:def 5;
then ( (1 - a) * x in W & a * y in W ) by RLSUB_1:29;
then A1: ((1 - a) * x) + (a * y) in W by RLSUB_1:28;
thus ((1 - a) * x) + (a * y) in Up W by A1, STRUCT_0:def 5; :: thesis: verum

end;

hence Up W is Affine by Def5; :: thesis: 0. V in the carrier of W
0. V in W by RLSUB_1:25;
hence 0. V in the carrier of W by STRUCT_0:def 5; :: thesis: verum