let V be RealLinearSpace; :: thesis: for A being Subset of V holds conv A = union { (Int B) where B is Subset of V : B c= A }

let A be Subset of V; :: thesis: conv A = union { (Int B) where B is Subset of V : B c= A }

defpred S_{1}[ Nat] means for S being finite Subset of V st card S <= $1 holds

conv S = union { (Int B) where B is Subset of V : B c= S } ;

set I = { (Int B) where B is Subset of V : B c= A } ;

A1: for A being Subset of V holds union { (Int B) where B is Subset of V : B c= A } c= conv A_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A20, A7);

let A be Subset of V; :: thesis: conv A = union { (Int B) where B is Subset of V : B c= A }

defpred S

conv S = union { (Int B) where B is Subset of V : B c= S } ;

set I = { (Int B) where B is Subset of V : B c= A } ;

A1: for A being Subset of V holds union { (Int B) where B is Subset of V : B c= A } c= conv A

proof

A7:
for n being Nat st S
let A be Subset of V; :: thesis: union { (Int B) where B is Subset of V : B c= A } c= conv A

set I = { (Int B) where B is Subset of V : B c= A } ;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in union { (Int B) where B is Subset of V : B c= A } or y in conv A )

assume y in union { (Int B) where B is Subset of V : B c= A } ; :: thesis: y in conv A

then consider x being set such that

A2: y in x and

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

consider B being Subset of V such that

A4: x = Int B and

A5: B c= A by A3;

A6: conv B c= conv A by A5, RLAFFIN1:3;

y in conv B by A2, A4, Def1;

hence y in conv A by A6; :: thesis: verum

end;set I = { (Int B) where B is Subset of V : B c= A } ;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in union { (Int B) where B is Subset of V : B c= A } or y in conv A )

assume y in union { (Int B) where B is Subset of V : B c= A } ; :: thesis: y in conv A

then consider x being set such that

A2: y in x and

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

consider B being Subset of V such that

A4: x = Int B and

A5: B c= A by A3;

A6: conv B c= conv A by A5, RLAFFIN1:3;

y in conv B by A2, A4, Def1;

hence y in conv A by A6; :: thesis: verum

S

proof

A20:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A8: S_{1}[n]
; :: thesis: S_{1}[n + 1]

let S be finite Subset of V; :: thesis: ( card S <= n + 1 implies conv S = union { (Int B) where B is Subset of V : B c= S } )

assume A9: card S <= n + 1 ; :: thesis: conv S = union { (Int B) where B is Subset of V : B c= S }

end;assume A8: S

let S be finite Subset of V; :: thesis: ( card S <= n + 1 implies conv S = union { (Int B) where B is Subset of V : B c= S } )

assume A9: card S <= n + 1 ; :: thesis: conv S = union { (Int B) where B is Subset of V : B c= S }

per cases
( card S <= n or card S = n + 1 )
by A9, NAT_1:8;

end;

suppose A10:
card S = n + 1
; :: thesis: conv S = union { (Int B) where B is Subset of V : B c= S }

set I = { (Int B) where B is Subset of V : B c= S } ;

A11: conv S c= union { (Int B) where B is Subset of V : B c= S }

hence conv S = union { (Int B) where B is Subset of V : B c= S } by A11; :: thesis: verum

end;A11: conv S c= union { (Int B) where B is Subset of V : B c= S }

proof

union { (Int B) where B is Subset of V : B c= S } c= conv S
by A1;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in conv S or x in union { (Int B) where B is Subset of V : B c= S } )

assume A12: x in conv S ; :: thesis: x in union { (Int B) where B is Subset of V : B c= S }

end;assume A12: x in conv S ; :: thesis: x in union { (Int B) where B is Subset of V : B c= S }

per cases
( for A being Subset of V st A c< S holds

not x in conv A or ex A being Subset of V st

( A c< S & x in conv A ) ) ;

end;

not x in conv A or ex A being Subset of V st

( A c< S & x in conv A ) ) ;

suppose
for A being Subset of V st A c< S holds

not x in conv A ; :: thesis: x in union { (Int B) where B is Subset of V : B c= S }

not x in conv A ; :: thesis: x in union { (Int B) where B is Subset of V : B c= S }

then
( Int S in { (Int B) where B is Subset of V : B c= S } & x in Int S )
by A12, Def1;

hence x in union { (Int B) where B is Subset of V : B c= S } by TARSKI:def 4; :: thesis: verum

end;hence x in union { (Int B) where B is Subset of V : B c= S } by TARSKI:def 4; :: thesis: verum

suppose
ex A being Subset of V st

( A c< S & x in conv A ) ; :: thesis: x in union { (Int B) where B is Subset of V : B c= S }

( A c< S & x in conv A ) ; :: thesis: x in union { (Int B) where B is Subset of V : B c= S }

then consider A being Subset of V such that

A13: A c< S and

A14: x in conv A ;

A15: A c= S by A13;

then reconsider A = A as finite Subset of V ;

card A < n + 1 by A10, A13, CARD_2:48;

then card A <= n by NAT_1:13;

then conv A = union { (Int B) where B is Subset of V : B c= A } by A8;

then consider Y being set such that

A16: x in Y and

A17: Y in { (Int B) where B is Subset of V : B c= A } by A14, TARSKI:def 4;

consider B being Subset of V such that

A18: Y = Int B and

A19: B c= A by A17;

B c= S by A15, A19;

then Int B in { (Int B) where B is Subset of V : B c= S } ;

hence x in union { (Int B) where B is Subset of V : B c= S } by A16, A18, TARSKI:def 4; :: thesis: verum

end;A13: A c< S and

A14: x in conv A ;

A15: A c= S by A13;

then reconsider A = A as finite Subset of V ;

card A < n + 1 by A10, A13, CARD_2:48;

then card A <= n by NAT_1:13;

then conv A = union { (Int B) where B is Subset of V : B c= A } by A8;

then consider Y being set such that

A16: x in Y and

A17: Y in { (Int B) where B is Subset of V : B c= A } by A14, TARSKI:def 4;

consider B being Subset of V such that

A18: Y = Int B and

A19: B c= A by A17;

B c= S by A15, A19;

then Int B in { (Int B) where B is Subset of V : B c= S } ;

hence x in union { (Int B) where B is Subset of V : B c= S } by A16, A18, TARSKI:def 4; :: thesis: verum

hence conv S = union { (Int B) where B is Subset of V : B c= S } by A11; :: thesis: verum

proof

A22:
for n being Nat holds S
let A be finite Subset of V; :: thesis: ( card A <= 0 implies conv A = union { (Int B) where B is Subset of V : B c= A } )

set I = { (Int B) where B is Subset of V : B c= A } ;

assume card A <= 0 ; :: thesis: conv A = union { (Int B) where B is Subset of V : B c= A }

then A is empty ;

then A21: conv A is empty ;

union { (Int B) where B is Subset of V : B c= A } c= conv A by A1;

hence conv A = union { (Int B) where B is Subset of V : B c= A } by A21; :: thesis: verum

end;set I = { (Int B) where B is Subset of V : B c= A } ;

assume card A <= 0 ; :: thesis: conv A = union { (Int B) where B is Subset of V : B c= A }

then A is empty ;

then A21: conv A is empty ;

union { (Int B) where B is Subset of V : B c= A } c= conv A by A1;

hence conv A = union { (Int B) where B is Subset of V : B c= A } by A21; :: thesis: verum

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: union { (Int B) where B is Subset of V : B c= A } c= conv A

thus
union { (Int B) where B is Subset of V : B c= A } c= conv A
by A1; :: thesis: verumlet x be object ; :: thesis: ( x in conv A implies x in union { (Int B) where B is Subset of V : B c= A } )

assume A23: x in conv A ; :: thesis: x in union { (Int B) where B is Subset of V : B c= A }

reconsider A1 = A as non empty Subset of V by A23;

conv A = { (Sum L) where L is Convex_Combination of A1 : L in ConvexComb V } by CONVEX3:5;

then consider L being Convex_Combination of A1 such that

A24: ( x = Sum L & L in ConvexComb V ) by A23;

reconsider C = Carrier L as non empty finite Subset of V by CONVEX1:21;

reconsider K = L as Linear_Combination of C by RLVECT_2:def 6;

K is convex ;

then x in { (Sum M) where M is Convex_Combination of C : M in ConvexComb V } by A24;

then A25: x in conv C by CONVEX3:5;

S_{1}[ card C]
by A22;

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

then consider y being set such that

A26: x in y and

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

consider B being Subset of V such that

A28: y = Int B and

A29: B c= C by A27;

C c= A by RLVECT_2:def 6;

then B c= A by A29;

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

hence x in union { (Int B) where B is Subset of V : B c= A } by A26, A28, TARSKI:def 4; :: thesis: verum

end;assume A23: x in conv A ; :: thesis: x in union { (Int B) where B is Subset of V : B c= A }

reconsider A1 = A as non empty Subset of V by A23;

conv A = { (Sum L) where L is Convex_Combination of A1 : L in ConvexComb V } by CONVEX3:5;

then consider L being Convex_Combination of A1 such that

A24: ( x = Sum L & L in ConvexComb V ) by A23;

reconsider C = Carrier L as non empty finite Subset of V by CONVEX1:21;

reconsider K = L as Linear_Combination of C by RLVECT_2:def 6;

K is convex ;

then x in { (Sum M) where M is Convex_Combination of C : M in ConvexComb V } by A24;

then A25: x in conv C by CONVEX3:5;

S

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

then consider y being set such that

A26: x in y and

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

consider B being Subset of V such that

A28: y = Int B and

A29: B c= C by A27;

C c= A by RLVECT_2:def 6;

then B c= A by A29;

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

hence x in union { (Int B) where B is Subset of V : B c= A } by A26, A28, TARSKI:def 4; :: thesis: verum