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;

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 )
;

end;

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 )

end;

( I c= Ia & Ia c= A & Affin Ia = Affin A )

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

end;

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 )

( 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;thus ( I c= I & I c= A & Affin I = Affin A ) by A3, A4; :: thesis: verum

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 )

( 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))

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

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;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

then reconsider pA = (- p) + A as Subset of (Lin ((- p) + A)) ;
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;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

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

A15:
pIA0 c= Affin pIA0
by Lm7;
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)} ;

end;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;

end;

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;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

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

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 )

( 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))

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

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;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

then
(- p) + I c= Up (Lin ((- p) + A))
by A19;
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;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

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

A34:
pI0 c= Affin pI0
by Lm7;
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)} ;

end;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;

end;

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;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

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