let V be RealUnitarySpace; :: thesis: for A being non empty Affine Subset of V st 0. V in A holds
A = the carrier of (Lin A)
let A be non empty Affine Subset of V; :: thesis: ( 0. V in A implies A = the carrier of (Lin A) )
assume 0. V in A ; :: thesis: A = the carrier of (Lin A)
then A1: A is Subspace-like by Th26;
for x being object st x in the carrier of (Lin A) holds
x in A

proof

let x be object ; :: thesis: ( x in the carrier of (Lin A) implies x in A )
assume x in the carrier of (Lin A) ; :: thesis: x in A
then x in Lin A ;
then A2: ex l being Linear_Combination of A st x = Sum l by RUSUB_3:1;
( ( for v, u being VECTOR of V st v in A & u in A holds
v + u in A ) & ( for a being Real
for v being VECTOR of V st v in A holds
a * v in A ) ) by A1;
then A is linearly-closed by RLSUB_1:def 1;
hence x in A by A2, RLVECT_2:29; :: thesis: verum

end;

then A3: the carrier of (Lin A) c= A ;
for x being object st x in A holds
x in the carrier of (Lin A) by RUSUB_3:2, STRUCT_0:def 5;
then A c= the carrier of (Lin A) ;
hence A = the carrier of (Lin A) by A3; :: thesis: verum