let V be RealLinearSpace; :: thesis: for A being Subset of V
for I being affinely-independent Subset of V st I c= A holds
ex Ia being affinely-independent Subset of V st
( I c= Ia & Ia c= A & Affin Ia = Affin A )
let A be Subset of V; :: thesis: for I being affinely-independent Subset of V st I c= A holds
ex Ia being affinely-independent Subset of V st
( I c= Ia & Ia c= A & Affin Ia = Affin A )
let I be affinely-independent Subset of V; :: thesis: ( I c= A implies ex Ia being affinely-independent Subset of V st
( I c= Ia & Ia c= A & Affin Ia = Affin A ) )
assume A1: I c= A ; :: thesis: ex Ia being affinely-independent Subset of V st
( I c= Ia & Ia c= A & Affin Ia = Affin A )
A2: A c= Affin A by Lm7;

per cases ( I is empty or not I is empty ) ;

suppose A3: I is empty ; :: thesis: ex Ia being affinely-independent Subset of V st
( I c= Ia & Ia c= A & Affin Ia = Affin A )

per cases ( A is empty or not A is empty ) ;

suppose A4: A is empty ; :: thesis: ex Ia being affinely-independent Subset of V st
( I c= Ia & Ia c= A & Affin Ia = Affin A )

take I ; :: thesis: ( I c= I & I c= A & Affin I = Affin A )
thus ( I c= I & I c= A & Affin I = Affin A ) by A3, A4; :: thesis: verum

end;

suppose not A is empty ; :: thesis: ex Ia being affinely-independent Subset of V st
( I c= Ia & Ia c= A & Affin Ia = Affin A )

then consider p being object such that
A5: p in A ;
reconsider p = p as Element of V by A5;
set L = Lin ((- p) + A);
(- p) + A c= [#] (Lin ((- p) + A))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (- p) + A or x in [#] (Lin ((- p) + A)) )
assume x in (- p) + A ; :: thesis: x in [#] (Lin ((- p) + A))
then x in Lin ((- p) + A) by RLVECT_3:15;
hence x in [#] (Lin ((- p) + A)) ; :: thesis: verum

end;

then reconsider pA = (- p) + A as Subset of (Lin ((- p) + A)) ;
Lin ((- p) + A) = Lin pA by RLVECT_5:20;
then consider Ia being Subset of (Lin ((- p) + A)) such that
A6: Ia c= pA and
A7: Ia is linearly-independent and
A8: Lin Ia = Lin ((- p) + A) by RLVECT_3:25;
[#] (Lin ((- p) + A)) c= [#] V by RLSUB_1:def 2;
then reconsider IA = Ia as Subset of V by XBOOLE_1:1;
set IA0 = IA \/ {(0. V)};
not 0. V in IA by A7, RLVECT_3:6, RLVECT_5:14;
then A9: (IA \/ {(0. V)}) \ {(0. V)} = IA by ZFMISC_1:117;
0. V in {(0. V)} by TARSKI:def 1;
then A10: 0. V in IA \/ {(0. V)} by XBOOLE_0:def 3;
IA is linearly-independent by A7, RLVECT_5:14;
then IA \/ {(0. V)} is affinely-independent by A9, A10, Th46;
then reconsider pIA0 = p + (IA \/ {(0. V)}) as affinely-independent Subset of V ;
take pIA0 ; :: thesis: ( I c= pIA0 & pIA0 c= A & Affin pIA0 = Affin A )
thus I c= pIA0 by A3; :: thesis: ( pIA0 c= A & Affin pIA0 = Affin A )
thus pIA0 c= A :: thesis: Affin pIA0 = Affin A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in pIA0 or x in A )
assume x in pIA0 ; :: thesis: x in A
then consider v being VECTOR of V such that
A11: x = p + v and
A12: v in IA \/ {(0. V)} ;

per cases ( v in IA or v in {(0. V)} ) by A12, XBOOLE_0:def 3;

suppose v in IA ; :: thesis: x in A

then v in { ((- p) + w) where w is VECTOR of V : w in A } by A6;
then consider w being VECTOR of V such that
A13: v = (- p) + w and
A14: w in A ;
x = (p + (- p)) + w by A11, A13, RLVECT_1:def 3
.= (0. V) + w by RLVECT_1:5
.= w ;
hence x in A by A14; :: thesis: verum

end;

suppose v in {(0. V)} ; :: thesis: x in A

then v = 0. V by TARSKI:def 1;
hence x in A by A5, A11; :: thesis: verum

end;

end;

end;

A15: pIA0 c= Affin pIA0 by Lm7;
A16: (- p) + pIA0 = ((- p) + p) + (IA \/ {(0. V)}) by Th5
.= (0. V) + (IA \/ {(0. V)}) by RLVECT_1:5
.= IA \/ {(0. V)} by Th6 ;
p + (0. V) = p ;
then p in pIA0 by A10;
hence Affin pIA0 = p + (Up (Lin (IA \/ {(0. V)}))) by A15, A16, Th57
.= p + (Up (Lin IA)) by Lm9
.= p + (Up (Lin ((- p) + A))) by A8, RLVECT_5:20
.= Affin A by A2, A5, Th57 ;
:: thesis: verum

end;

end;

end;

suppose not I is empty ; :: thesis: ex Ia being affinely-independent Subset of V st
( I c= Ia & Ia c= A & Affin Ia = Affin A )

then consider p being object such that
A17: p in I ;
reconsider p = p as Element of V by A17;
A18: ((- p) + I) \ {(0. V)} is linearly-independent by A17, Th41;
A19: (- p) + I c= (- p) + A by A1, RLTOPSP1:8;
set L = Lin ((- p) + A);
A20: ((- p) + I) \ {(0. V)} c= (- p) + I by XBOOLE_1:36;
A21: (- p) + A c= Up (Lin ((- p) + A))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (- p) + A or x in Up (Lin ((- p) + A)) )
assume x in (- p) + A ; :: thesis: x in Up (Lin ((- p) + A))
then x in Lin ((- p) + A) by RLVECT_3:15;
hence x in Up (Lin ((- p) + A)) ; :: thesis: verum

end;

then (- p) + I c= Up (Lin ((- p) + A)) by A19;
then reconsider pI0 = ((- p) + I) \ {(0. V)}, pA = (- p) + A as Subset of (Lin ((- p) + A)) by A20, A21, XBOOLE_1:1;
( Lin ((- p) + A) = Lin pA & pI0 c= pA ) by A19, A20, RLVECT_5:20;
then consider i being linearly-independent Subset of (Lin ((- p) + A)) such that
A22: pI0 c= i and
A23: i c= pA and
A24: Lin i = Lin ((- p) + A) by A18, Th15, RLVECT_5:15;
reconsider Ia = i as linearly-independent Subset of V by RLVECT_5:14;
set I0 = Ia \/ {(0. V)};
A25: 0. V in {(0. V)} by TARSKI:def 1;
not 0. V in Ia by RLVECT_3:6;
then ( (Ia \/ {(0. V)}) \ {(0. V)} = Ia & 0. V in Ia \/ {(0. V)} ) by A25, XBOOLE_0:def 3, ZFMISC_1:117;
then Ia \/ {(0. V)} is affinely-independent by Th46;
then reconsider pI0 = p + (Ia \/ {(0. V)}) as affinely-independent Subset of V ;
take pI0 ; :: thesis: ( I c= pI0 & pI0 c= A & Affin pI0 = Affin A )
A26: (- p) + p = 0. V by RLVECT_1:5;
then A27: p + ((- p) + I) = (0. V) + I by Th5
.= I by Th6 ;
0. V in { ((- p) + v) where v is Element of V : v in I } by A17, A26;
then (((- p) + I) \ {(0. V)}) \/ {(0. V)} = (- p) + I by ZFMISC_1:116;
then A28: (- p) + I c= Ia \/ {(0. V)} by A22, XBOOLE_1:9;
hence I c= pI0 by A27, RLTOPSP1:8; :: thesis: ( pI0 c= A & Affin pI0 = Affin A )
p + ((- p) + I) c= pI0 by A28, RLTOPSP1:8;
then A29: p in pI0 by A17, A27;
thus pI0 c= A :: thesis: Affin pI0 = Affin A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in pI0 or x in A )
assume x in pI0 ; :: thesis: x in A
then consider v being VECTOR of V such that
A30: x = p + v and
A31: v in Ia \/ {(0. V)} ;

per cases ( v in Ia or v in {(0. V)} ) by A31, XBOOLE_0:def 3;

suppose v in Ia ; :: thesis: x in A

then v in { ((- p) + w) where w is VECTOR of V : w in A } by A23;
then consider w being VECTOR of V such that
A32: v = (- p) + w and
A33: w in A ;
x = (p + (- p)) + w by A30, A32, RLVECT_1:def 3
.= (0. V) + w by RLVECT_1:5
.= w ;
hence x in A by A33; :: thesis: verum

end;

suppose v in {(0. V)} ; :: thesis: x in A

then v = 0. V by TARSKI:def 1;
then x = p by A30;
hence x in A by A1, A17; :: thesis: verum

end;

end;

end;

A34: pI0 c= Affin pI0 by Lm7;
A35: p in A by A1, A17;
(- p) + pI0 = (0. V) + (Ia \/ {(0. V)}) by A26, Th5
.= Ia \/ {(0. V)} by Th6 ;
hence Affin pI0 = p + (Up (Lin (Ia \/ {(0. V)}))) by A29, A34, Th57
.= p + (Up (Lin Ia)) by Lm9
.= p + (Up (Lin ((- p) + A))) by A24, RLVECT_5:20
.= Affin A by A2, A35, Th57 ;
:: thesis: verum

end;

end;