let V be RealLinearSpace; :: thesis: for A being Subset of V holds conv A = (Int A) \/ (union { (conv (A \ {v})) where v is VECTOR of V : v in A } )

let A be Subset of V; :: thesis: conv A = (Int A) \/ (union { (conv (A \ {v})) where v is VECTOR of V : v in A } )

set I = { (conv (A \ {v})) where v is VECTOR of V : v in A } ;

then A13: ( x in Int A or x in union { (conv (A \ {v})) where v is VECTOR of V : v in A } ) by XBOOLE_0:def 3;

Int A c= conv A by Lm2;

hence x in conv A by A9, A13; :: thesis: verum

let A be Subset of V; :: thesis: conv A = (Int A) \/ (union { (conv (A \ {v})) where v is VECTOR of V : v in A } )

set I = { (conv (A \ {v})) where v is VECTOR of V : v in A } ;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: (Int A) \/ (union { (conv (A \ {v})) where v is VECTOR of V : v in A } ) c= conv A

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Int A) \/ (union { (conv (A \ {v})) where v is VECTOR of V : v in A } ) or x in conv A )let x be object ; :: thesis: ( x in conv A implies b_{1} in (Int A) \/ (union { (conv (A \ {b_{2}})) where v is VECTOR of V : b_{2} in A } ) )

assume x in conv A ; :: thesis: b_{1} in (Int A) \/ (union { (conv (A \ {b_{2}})) where v is VECTOR of V : b_{2} in A } )

then x in union { (Int B) where B is Subset of V : B c= A } by Th8;

then consider y being set such that

A1: x in y and

A2: y in { (Int B) where B is Subset of V : B c= A } by TARSKI:def 4;

consider B being Subset of V such that

A3: y = Int B and

A4: B c= A by A2;

end;assume x in conv A ; :: thesis: b

then x in union { (Int B) where B is Subset of V : B c= A } by Th8;

then consider y being set such that

A1: x in y and

A2: y in { (Int B) where B is Subset of V : B c= A } by TARSKI:def 4;

consider B being Subset of V such that

A3: y = Int B and

A4: B c= A by A2;

per cases
( A = B or B <> A )
;

end;

suppose
A = B
; :: thesis: b_{1} in (Int A) \/ (union { (conv (A \ {b_{2}})) where v is VECTOR of V : b_{2} in A } )

hence
x in (Int A) \/ (union { (conv (A \ {v})) where v is VECTOR of V : v in A } )
by A1, A3, XBOOLE_0:def 3; :: thesis: verum

end;suppose
B <> A
; :: thesis: b_{1} in (Int A) \/ (union { (conv (A \ {b_{2}})) where v is VECTOR of V : b_{2} in A } )

then
B c< A
by A4;

then consider y being object such that

A5: y in A and

A6: not y in B by XBOOLE_0:6;

reconsider y = y as Element of V by A5;

A7: conv (A \ {y}) in { (conv (A \ {v})) where v is VECTOR of V : v in A } by A5;

B c= A \ {y} by A4, A6, ZFMISC_1:34;

then A8: conv B c= conv (A \ {y}) by RLAFFIN1:3;

x in conv B by A1, A3, Def1;

then x in union { (conv (A \ {v})) where v is VECTOR of V : v in A } by A7, A8, TARSKI:def 4;

hence x in (Int A) \/ (union { (conv (A \ {v})) where v is VECTOR of V : v in A } ) by XBOOLE_0:def 3; :: thesis: verum

end;then consider y being object such that

A5: y in A and

A6: not y in B by XBOOLE_0:6;

reconsider y = y as Element of V by A5;

A7: conv (A \ {y}) in { (conv (A \ {v})) where v is VECTOR of V : v in A } by A5;

B c= A \ {y} by A4, A6, ZFMISC_1:34;

then A8: conv B c= conv (A \ {y}) by RLAFFIN1:3;

x in conv B by A1, A3, Def1;

then x in union { (conv (A \ {v})) where v is VECTOR of V : v in A } by A7, A8, TARSKI:def 4;

hence x in (Int A) \/ (union { (conv (A \ {v})) where v is VECTOR of V : v in A } ) by XBOOLE_0:def 3; :: thesis: verum

A9: now :: thesis: ( x in union { (conv (A \ {v})) where v is VECTOR of V : v in A } implies x in conv A )

assume
x in (Int A) \/ (union { (conv (A \ {v})) where v is VECTOR of V : v in A } )
; :: thesis: x in conv Aassume
x in union { (conv (A \ {v})) where v is VECTOR of V : v in A }
; :: thesis: x in conv A

then consider y being set such that

A10: x in y and

A11: y in { (conv (A \ {v})) where v is VECTOR of V : v in A } by TARSKI:def 4;

consider v being VECTOR of V such that

A12: y = conv (A \ {v}) and

v in A by A11;

conv (A \ {v}) c= conv A by RLAFFIN1:3, XBOOLE_1:36;

hence x in conv A by A10, A12; :: thesis: verum

end;then consider y being set such that

A10: x in y and

A11: y in { (conv (A \ {v})) where v is VECTOR of V : v in A } by TARSKI:def 4;

consider v being VECTOR of V such that

A12: y = conv (A \ {v}) and

v in A by A11;

conv (A \ {v}) c= conv A by RLAFFIN1:3, XBOOLE_1:36;

hence x in conv A by A10, A12; :: thesis: verum

then A13: ( x in Int A or x in union { (conv (A \ {v})) where v is VECTOR of V : v in A } ) by XBOOLE_0:def 3;

Int A c= conv A by Lm2;

hence x in conv A by A9, A13; :: thesis: verum