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 } ;
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 ; :: thesis: ( x in conv A implies b1 in (Int A) \/ (union { (conv (A \ {b2})) where v is VECTOR of V : b2 in A } ) )
assume x in conv A ; :: thesis: b1 in (Int A) \/ (union { (conv (A \ {b2})) where v is VECTOR of V : b2 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;
per cases ( A = B or B <> A ) ;
suppose A = B ; :: thesis: b1 in (Int A) \/ (union { (conv (A \ {b2})) where v is VECTOR of V : b2 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: b1 in (Int A) \/ (union { (conv (A \ {b2})) where v is VECTOR of V : b2 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;
end;
end;
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 )
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 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;
assume x in (Int A) \/ (union { (conv (A \ {v})) where v is VECTOR of V : v in A } ) ; :: thesis: x in conv 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