let V be RealLinearSpace; :: thesis: for Sf being c=-linear finite finite-membered Subset-Family of V st Sf is with_non-empty_elements & (card Sf) + 1 = card (union Sf) & union Sf is affinely-independent holds

card { S1 where S1 is Simplex of card Sf, BCS (Complex_of {(union Sf)}) : (center_of_mass V) .: Sf c= S1 } = 2

let S be c=-linear finite finite-membered Subset-Family of V; :: thesis: ( S is with_non-empty_elements & (card S) + 1 = card (union S) & union S is affinely-independent implies card { S1 where S1 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S1 } = 2 )

assume that

A1: S is with_non-empty_elements and

A2: (card S) + 1 = card (union S) and

A3: union S is affinely-independent ; :: thesis: card { S1 where S1 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S1 } = 2

set B = center_of_mass V;

reconsider U = union S as finite affinely-independent Subset of V by A3;

reconsider s = S as Subset-Family of U by ZFMISC_1:82;

A4: not S is empty by A2, ZFMISC_1:2;

then consider ss1 being Subset-Family of U such that

A5: s c= ss1 and

A6: ( ss1 is with_non-empty_elements & ss1 is c=-linear ) and

A7: card ss1 = card U and

A8: for X being set st X in ss1 & card X <> 1 holds

ex x being set st

( x in X & X \ {x} in ss1 ) by A1, SIMPLEX0:9, SIMPLEX0:13;

card (ss1 \ s) = ((card S) + 1) - (card S) by A2, A5, A7, CARD_2:44;

then consider x being object such that

A9: ss1 \ s = {x} by CARD_2:42;

reconsider c = card U as ExtReal ;

set CU = Complex_of {U};

set TC = the topology of (Complex_of {U});

A10: the topology of (Complex_of {U}) = bool U by SIMPLEX0:4;

then reconsider ss = ss1 as Subset-Family of (Complex_of {U}) by XBOOLE_1:1;

set BC = BCS (Complex_of {U});

reconsider cc = (card U) - 1 as ExtReal ;

A11: |.(Complex_of {U}).| c= [#] (Complex_of {U}) ;

then A12: BCS (Complex_of {U}) = subdivision ((center_of_mass V),(Complex_of {U})) by Def5;

then A13: [#] (BCS (Complex_of {U})) = [#] (Complex_of {U}) by SIMPLEX0:def 20;

then reconsider Bss = (center_of_mass V) .: ss as Subset of (BCS (Complex_of {U})) ;

A14: ss is simplex-like

then A16: card Bss = cc + 1 by A2, XXREAL_3:def 2;

A17: x in {x} by TARSKI:def 1;

then A18: x in ss1 by A9, XBOOLE_0:def 5;

A19: not x in s by A9, A17, XBOOLE_0:def 5;

reconsider x = x as finite Subset of V by A9, A17, XBOOLE_1:1;

degree (Complex_of {U}) = c - 1 by SIMPLEX0:26

.= (card U) + (- 1) by XXREAL_3:def 2 ;

then A20: cc = degree (BCS (Complex_of {U})) by A11, Th31;

Bss is simplex-like by A6, A12, A14, SIMPLEX0:def 20;

then A21: Bss is Simplex of (card U) - 1, BCS (Complex_of {U}) by A2, A16, A20, SIMPLEX0:def 18;

x <> {} by A6, A18;

then reconsider c1 = (card x) - 1 as Element of NAT by NAT_1:20;

ex xm being set st

( ( xm in s or xm = {} ) & card xm = (card x) - 1 & ( for y being set st y in s & y c= x holds

y c= xm ) )

A32: ( xm in s or xm = {} ) and

A33: card xm = (card x) - 1 and

A34: for y being set st y in s & y c= x holds

y c= xm ;

A35: U in S by A4, SIMPLEX0:9;

then ( union ss1 c= U & U c= union ss ) by A5, ZFMISC_1:74;

then A36: union ss = U ;

x c< U by A9, A17, A19, A35;

then card x < card U by CARD_2:48;

then (card x) + 1 <= card U by NAT_1:13;

then consider xM being set such that

A37: xM in ss and

A38: card xM = (card x) + 1 by A6, A36, A21, Th36;

reconsider xm = xm as finite Subset of V by A32, XBOOLE_1:2;

reconsider xM = xM as finite Subset of V by A37;

A39: not xM c= xm

then A41: xm c= xM by A39;

then card (xM \ xm) = (card xM) - (card xm) by CARD_2:44;

then consider x1, x2 being object such that

A42: x1 <> x2 and

A43: xM \ xm = {x1,x2} by A33, A38, CARD_2:60;

A44: x1 in {x1,x2} by TARSKI:def 2;

A45: x2 in {x1,x2} by TARSKI:def 2;

then reconsider x1 = x1, x2 = x2 as Element of V by A43, A44;

set xm1 = xm \/ {x1};

set xm2 = xm \/ {x2};

reconsider S1 = S \/ {(xm \/ {x1})}, S2 = S \/ {(xm \/ {x2})} as Subset-Family of (Complex_of {U}) ;

reconsider BS1 = (center_of_mass V) .: S1, BS2 = (center_of_mass V) .: S2 as Subset of (BCS (Complex_of {U})) by A13;

A46: BS1 = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {(xm \/ {x1})}) by RELAT_1:120;

A47: not x1 in xm by A43, A44, XBOOLE_0:def 5;

then A48: card (xm \/ {x1}) = (card xm) + 1 by CARD_2:41;

A49: not xm \/ {x1} in S

then A51: card (xm \/ {x2}) = (card xm) + 1 by CARD_2:41;

A52: not xm \/ {x2} in S

then {x2} c= xM by ZFMISC_1:31;

then A54: xm \/ {x2} c= xM by A41, XBOOLE_1:8;

A55: S2 c= bool U

then A58: card BS2 = (card S) + 1 by A52, CARD_2:41;

x1 in xM by A43, A44, XBOOLE_0:def 5;

then {x1} c= xM by ZFMISC_1:31;

then A59: xm \/ {x1} c= xM by A41, XBOOLE_1:8;

A60: S1 c= bool U

A63: S1 is simplex-like

then A64: card BS1 = (card S) + 1 by A49, CARD_2:41;

A65: ( xm c= xm \/ {x1} & xm c= xm \/ {x2} ) by XBOOLE_1:7;

A66: for y1 being set st y1 in S holds

( y1,xm \/ {x1} are_c=-comparable & y1,xm \/ {x2} are_c=-comparable )

then A77: BS1 is Simplex of (card U) - 1, BCS (Complex_of {U}) by A2, A15, A16, A20, A64, SIMPLEX0:def 18;

set SS = { S3 where S3 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S3 } ;

(center_of_mass V) .: S c= ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {(xm \/ {x1})}) by XBOOLE_1:7;

then A78: BS1 in { S3 where S3 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S3 } by A2, A46, A77;

A79: BS2 = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {(xm \/ {x2})}) by RELAT_1:120;

A80: { S3 where S3 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S3 } c= {BS1,BS2}

A110: BS1 <> BS2

then A126: BS2 is Simplex of (card U) - 1, BCS (Complex_of {U}) by A2, A15, A16, A20, A58, SIMPLEX0:def 18;

(center_of_mass V) .: S c= ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {(xm \/ {x2})}) by XBOOLE_1:7;

then BS2 in { S3 where S3 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S3 } by A2, A79, A126;

then {BS1,BS2} c= { S3 where S3 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S3 } by A78, ZFMISC_1:32;

then { S3 where S3 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S3 } = {BS1,BS2} by A80;

hence card { S1 where S1 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S1 } = 2 by A110, CARD_2:57; :: thesis: verum

card { S1 where S1 is Simplex of card Sf, BCS (Complex_of {(union Sf)}) : (center_of_mass V) .: Sf c= S1 } = 2

let S be c=-linear finite finite-membered Subset-Family of V; :: thesis: ( S is with_non-empty_elements & (card S) + 1 = card (union S) & union S is affinely-independent implies card { S1 where S1 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S1 } = 2 )

assume that

A1: S is with_non-empty_elements and

A2: (card S) + 1 = card (union S) and

A3: union S is affinely-independent ; :: thesis: card { S1 where S1 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S1 } = 2

set B = center_of_mass V;

reconsider U = union S as finite affinely-independent Subset of V by A3;

reconsider s = S as Subset-Family of U by ZFMISC_1:82;

A4: not S is empty by A2, ZFMISC_1:2;

then consider ss1 being Subset-Family of U such that

A5: s c= ss1 and

A6: ( ss1 is with_non-empty_elements & ss1 is c=-linear ) and

A7: card ss1 = card U and

A8: for X being set st X in ss1 & card X <> 1 holds

ex x being set st

( x in X & X \ {x} in ss1 ) by A1, SIMPLEX0:9, SIMPLEX0:13;

card (ss1 \ s) = ((card S) + 1) - (card S) by A2, A5, A7, CARD_2:44;

then consider x being object such that

A9: ss1 \ s = {x} by CARD_2:42;

reconsider c = card U as ExtReal ;

set CU = Complex_of {U};

set TC = the topology of (Complex_of {U});

A10: the topology of (Complex_of {U}) = bool U by SIMPLEX0:4;

then reconsider ss = ss1 as Subset-Family of (Complex_of {U}) by XBOOLE_1:1;

set BC = BCS (Complex_of {U});

reconsider cc = (card U) - 1 as ExtReal ;

A11: |.(Complex_of {U}).| c= [#] (Complex_of {U}) ;

then A12: BCS (Complex_of {U}) = subdivision ((center_of_mass V),(Complex_of {U})) by Def5;

then A13: [#] (BCS (Complex_of {U})) = [#] (Complex_of {U}) by SIMPLEX0:def 20;

then reconsider Bss = (center_of_mass V) .: ss as Subset of (BCS (Complex_of {U})) ;

A14: ss is simplex-like

proof

then A15:
card Bss = card U
by A6, A7, Th33;
let A be Subset of (Complex_of {U}); :: according to TOPS_2:def 1 :: thesis: ( not A in ss or not A is dependent )

assume A in ss ; :: thesis: not A is dependent

hence not A is dependent by A10; :: thesis: verum

end;assume A in ss ; :: thesis: not A is dependent

hence not A is dependent by A10; :: thesis: verum

then A16: card Bss = cc + 1 by A2, XXREAL_3:def 2;

A17: x in {x} by TARSKI:def 1;

then A18: x in ss1 by A9, XBOOLE_0:def 5;

A19: not x in s by A9, A17, XBOOLE_0:def 5;

reconsider x = x as finite Subset of V by A9, A17, XBOOLE_1:1;

degree (Complex_of {U}) = c - 1 by SIMPLEX0:26

.= (card U) + (- 1) by XXREAL_3:def 2 ;

then A20: cc = degree (BCS (Complex_of {U})) by A11, Th31;

Bss is simplex-like by A6, A12, A14, SIMPLEX0:def 20;

then A21: Bss is Simplex of (card U) - 1, BCS (Complex_of {U}) by A2, A16, A20, SIMPLEX0:def 18;

x <> {} by A6, A18;

then reconsider c1 = (card x) - 1 as Element of NAT by NAT_1:20;

ex xm being set st

( ( xm in s or xm = {} ) & card xm = (card x) - 1 & ( for y being set st y in s & y c= x holds

y c= xm ) )

proof
end;

then consider xm being set such that per cases
( card x = 1 or card x <> 1 )
;

end;

suppose A22:
card x = 1
; :: thesis: ex xm being set st

( ( xm in s or xm = {} ) & card xm = (card x) - 1 & ( for y being set st y in s & y c= x holds

y c= xm ) )

( ( xm in s or xm = {} ) & card xm = (card x) - 1 & ( for y being set st y in s & y c= x holds

y c= xm ) )

then A23:
ex z being object st x = {z}
by CARD_2:42;

take xm = {} ; :: thesis: ( ( xm in s or xm = {} ) & card xm = (card x) - 1 & ( for y being set st y in s & y c= x holds

y c= xm ) )

thus ( ( xm in s or xm = {} ) & card xm = (card x) - 1 ) by A22; :: thesis: for y being set st y in s & y c= x holds

y c= xm

let y be set ; :: thesis: ( y in s & y c= x implies y c= xm )

assume that

A24: y in s and

A25: y c= x ; :: thesis: y c= xm

y <> x by A9, A17, A24, XBOOLE_0:def 5;

hence y c= xm by A23, A25, ZFMISC_1:33; :: thesis: verum

end;take xm = {} ; :: thesis: ( ( xm in s or xm = {} ) & card xm = (card x) - 1 & ( for y being set st y in s & y c= x holds

y c= xm ) )

thus ( ( xm in s or xm = {} ) & card xm = (card x) - 1 ) by A22; :: thesis: for y being set st y in s & y c= x holds

y c= xm

let y be set ; :: thesis: ( y in s & y c= x implies y c= xm )

assume that

A24: y in s and

A25: y c= x ; :: thesis: y c= xm

y <> x by A9, A17, A24, XBOOLE_0:def 5;

hence y c= xm by A23, A25, ZFMISC_1:33; :: thesis: verum

suppose
card x <> 1
; :: thesis: ex xm being set st

( ( xm in s or xm = {} ) & card xm = (card x) - 1 & ( for y being set st y in s & y c= x holds

y c= xm ) )

( ( xm in s or xm = {} ) & card xm = (card x) - 1 & ( for y being set st y in s & y c= x holds

y c= xm ) )

then consider z being set such that

A26: z in x and

A27: x \ {z} in ss1 by A8, A18;

take xm = x \ {z}; :: thesis: ( ( xm in s or xm = {} ) & card xm = (card x) - 1 & ( for y being set st y in s & y c= x holds

y c= xm ) )

A28: x = xm \/ {z} by A26, ZFMISC_1:116;

xm in s

y c= xm ) )

card x = c1 + 1 ;

hence card xm = (card x) - 1 by A26, STIRL2_1:55; :: thesis: for y being set st y in s & y c= x holds

y c= xm

let y be set ; :: thesis: ( y in s & y c= x implies y c= xm )

assume that

A29: y in s and

A30: y c= x ; :: thesis: y c= xm

assume A31: not y c= xm ; :: thesis: contradiction

xm,y are_c=-comparable by A5, A6, A27, A29;

then xm c= y by A31;

hence contradiction by A19, A28, A29, A30, A31, ZFMISC_1:138; :: thesis: verum

end;A26: z in x and

A27: x \ {z} in ss1 by A8, A18;

take xm = x \ {z}; :: thesis: ( ( xm in s or xm = {} ) & card xm = (card x) - 1 & ( for y being set st y in s & y c= x holds

y c= xm ) )

A28: x = xm \/ {z} by A26, ZFMISC_1:116;

xm in s

proof

hence
( xm in s or xm = {} )
; :: thesis: ( card xm = (card x) - 1 & ( for y being set st y in s & y c= x holds
assume
not xm in s
; :: thesis: contradiction

then xm in ss1 \ s by A27, XBOOLE_0:def 5;

then xm = x by A9, TARSKI:def 1;

hence contradiction by A26, ZFMISC_1:56; :: thesis: verum

end;then xm in ss1 \ s by A27, XBOOLE_0:def 5;

then xm = x by A9, TARSKI:def 1;

hence contradiction by A26, ZFMISC_1:56; :: thesis: verum

y c= xm ) )

card x = c1 + 1 ;

hence card xm = (card x) - 1 by A26, STIRL2_1:55; :: thesis: for y being set st y in s & y c= x holds

y c= xm

let y be set ; :: thesis: ( y in s & y c= x implies y c= xm )

assume that

A29: y in s and

A30: y c= x ; :: thesis: y c= xm

assume A31: not y c= xm ; :: thesis: contradiction

xm,y are_c=-comparable by A5, A6, A27, A29;

then xm c= y by A31;

hence contradiction by A19, A28, A29, A30, A31, ZFMISC_1:138; :: thesis: verum

A32: ( xm in s or xm = {} ) and

A33: card xm = (card x) - 1 and

A34: for y being set st y in s & y c= x holds

y c= xm ;

A35: U in S by A4, SIMPLEX0:9;

then ( union ss1 c= U & U c= union ss ) by A5, ZFMISC_1:74;

then A36: union ss = U ;

x c< U by A9, A17, A19, A35;

then card x < card U by CARD_2:48;

then (card x) + 1 <= card U by NAT_1:13;

then consider xM being set such that

A37: xM in ss and

A38: card xM = (card x) + 1 by A6, A36, A21, Th36;

reconsider xm = xm as finite Subset of V by A32, XBOOLE_1:2;

reconsider xM = xM as finite Subset of V by A37;

A39: not xM c= xm

proof

A40:
xM in s
assume
xM c= xm
; :: thesis: contradiction

then (card x) + 1 <= (card x) + (- 1) by A33, A38, NAT_1:43;

hence contradiction by XREAL_1:6; :: thesis: verum

end;then (card x) + 1 <= (card x) + (- 1) by A33, A38, NAT_1:43;

hence contradiction by XREAL_1:6; :: thesis: verum

proof

then
( xm,xM are_c=-comparable or xm c= xM )
by A32, ORDINAL1:def 8;
assume
not xM in s
; :: thesis: contradiction

then xM in ss \ s by A37, XBOOLE_0:def 5;

then xM = x by A9, TARSKI:def 1;

hence contradiction by A38; :: thesis: verum

end;then xM in ss \ s by A37, XBOOLE_0:def 5;

then xM = x by A9, TARSKI:def 1;

hence contradiction by A38; :: thesis: verum

then A41: xm c= xM by A39;

then card (xM \ xm) = (card xM) - (card xm) by CARD_2:44;

then consider x1, x2 being object such that

A42: x1 <> x2 and

A43: xM \ xm = {x1,x2} by A33, A38, CARD_2:60;

A44: x1 in {x1,x2} by TARSKI:def 2;

A45: x2 in {x1,x2} by TARSKI:def 2;

then reconsider x1 = x1, x2 = x2 as Element of V by A43, A44;

set xm1 = xm \/ {x1};

set xm2 = xm \/ {x2};

reconsider S1 = S \/ {(xm \/ {x1})}, S2 = S \/ {(xm \/ {x2})} as Subset-Family of (Complex_of {U}) ;

reconsider BS1 = (center_of_mass V) .: S1, BS2 = (center_of_mass V) .: S2 as Subset of (BCS (Complex_of {U})) by A13;

A46: BS1 = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {(xm \/ {x1})}) by RELAT_1:120;

A47: not x1 in xm by A43, A44, XBOOLE_0:def 5;

then A48: card (xm \/ {x1}) = (card xm) + 1 by CARD_2:41;

A49: not xm \/ {x1} in S

proof

not x2 in xm
by A43, A45, XBOOLE_0:def 5;
assume A50:
xm \/ {x1} in S
; :: thesis: contradiction

then x,xm \/ {x1} are_c=-comparable by A5, A6, A18;

then ( x c= xm \/ {x1} or xm \/ {x1} c= x ) ;

hence contradiction by A19, A33, A48, A50, CARD_2:102; :: thesis: verum

end;then x,xm \/ {x1} are_c=-comparable by A5, A6, A18;

then ( x c= xm \/ {x1} or xm \/ {x1} c= x ) ;

hence contradiction by A19, A33, A48, A50, CARD_2:102; :: thesis: verum

then A51: card (xm \/ {x2}) = (card xm) + 1 by CARD_2:41;

A52: not xm \/ {x2} in S

proof

x2 in xM
by A43, A45, XBOOLE_0:def 5;
assume A53:
xm \/ {x2} in S
; :: thesis: contradiction

then x,xm \/ {x2} are_c=-comparable by A5, A6, A18;

then ( x c= xm \/ {x2} or xm \/ {x2} c= x ) ;

hence contradiction by A19, A33, A51, A53, CARD_2:102; :: thesis: verum

end;then x,xm \/ {x2} are_c=-comparable by A5, A6, A18;

then ( x c= xm \/ {x2} or xm \/ {x2} c= x ) ;

hence contradiction by A19, A33, A51, A53, CARD_2:102; :: thesis: verum

then {x2} c= xM by ZFMISC_1:31;

then A54: xm \/ {x2} c= xM by A41, XBOOLE_1:8;

A55: S2 c= bool U

proof

A57:
S2 is simplex-like
let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in S2 or A in bool U )

assume A56: A in S2 ; :: thesis: A in bool U

reconsider AA = A as set by TARSKI:1;

end;assume A56: A in S2 ; :: thesis: A in bool U

reconsider AA = A as set by TARSKI:1;

proof

then
card BS2 = card S2
by A1, Th33;
let A be Subset of (Complex_of {U}); :: according to TOPS_2:def 1 :: thesis: ( not A in S2 or not A is dependent )

assume A in S2 ; :: thesis: not A is dependent

hence not A is dependent by A10, A55; :: thesis: verum

end;assume A in S2 ; :: thesis: not A is dependent

hence not A is dependent by A10, A55; :: thesis: verum

then A58: card BS2 = (card S) + 1 by A52, CARD_2:41;

x1 in xM by A43, A44, XBOOLE_0:def 5;

then {x1} c= xM by ZFMISC_1:31;

then A59: xm \/ {x1} c= xM by A41, XBOOLE_1:8;

A60: S1 c= bool U

proof

then A62:
BS1 = ((center_of_mass V) | the topology of (Complex_of {U})) .: S1
by A10, RELAT_1:129;
let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in S1 or A in bool U )

assume A61: A in S1 ; :: thesis: A in bool U

reconsider AA = A as set by TARSKI:1;

end;assume A61: A in S1 ; :: thesis: A in bool U

reconsider AA = A as set by TARSKI:1;

A63: S1 is simplex-like

proof

then
card BS1 = card S1
by A1, Th33;
let A be Subset of (Complex_of {U}); :: according to TOPS_2:def 1 :: thesis: ( not A in S1 or not A is dependent )

assume A in S1 ; :: thesis: not A is dependent

hence not A is dependent by A10, A60; :: thesis: verum

end;assume A in S1 ; :: thesis: not A is dependent

hence not A is dependent by A10, A60; :: thesis: verum

then A64: card BS1 = (card S) + 1 by A49, CARD_2:41;

A65: ( xm c= xm \/ {x1} & xm c= xm \/ {x2} ) by XBOOLE_1:7;

A66: for y1 being set st y1 in S holds

( y1,xm \/ {x1} are_c=-comparable & y1,xm \/ {x2} are_c=-comparable )

proof

S1 is c=-linear
let y1 be set ; :: thesis: ( y1 in S implies ( y1,xm \/ {x1} are_c=-comparable & y1,xm \/ {x2} are_c=-comparable ) )

assume A67: y1 in S ; :: thesis: ( y1,xm \/ {x1} are_c=-comparable & y1,xm \/ {x2} are_c=-comparable )

then A68: xM,y1 are_c=-comparable by A40, ORDINAL1:def 8;

end;assume A67: y1 in S ; :: thesis: ( y1,xm \/ {x1} are_c=-comparable & y1,xm \/ {x2} are_c=-comparable )

then A68: xM,y1 are_c=-comparable by A40, ORDINAL1:def 8;

per cases
( xM c= y1 or xM = y1 or ( y1 c= xM & xM <> y1 ) )
by A68;

end;

suppose
( xM c= y1 or xM = y1 )
; :: thesis: ( y1,xm \/ {x1} are_c=-comparable & y1,xm \/ {x2} are_c=-comparable )

then
( xm \/ {x1} c= y1 & xm \/ {x2} c= y1 )
by A54, A59;

hence ( y1,xm \/ {x1} are_c=-comparable & y1,xm \/ {x2} are_c=-comparable ) ; :: thesis: verum

end;hence ( y1,xm \/ {x1} are_c=-comparable & y1,xm \/ {x2} are_c=-comparable ) ; :: thesis: verum

suppose A69:
( y1 c= xM & xM <> y1 )
; :: thesis: ( y1,xm \/ {x1} are_c=-comparable & y1,xm \/ {x2} are_c=-comparable )

then reconsider y1 = y1 as finite set ;

A70: y1 c< xM by A69;

A71: not x c= y1

then y1,x are_c=-comparable by A5, A6, A67;

then y1 c= x by A71;

then y1 c= xm by A34, A67;

then ( y1 c= xm \/ {x1} & y1 c= xm \/ {x2} ) by A65;

hence ( y1,xm \/ {x1} are_c=-comparable & y1,xm \/ {x2} are_c=-comparable ) ; :: thesis: verum

end;A70: y1 c< xM by A69;

A71: not x c= y1

proof

x in ss
by A9, A17, XBOOLE_0:def 5;
A72:
card y1 < card xM
by A70, CARD_2:48;

assume A73: x c= y1 ; :: thesis: contradiction

then card x <= card y1 by NAT_1:43;

then card x = card y1 by A38, A72, NAT_1:9;

hence contradiction by A19, A67, A73, CARD_2:102; :: thesis: verum

end;assume A73: x c= y1 ; :: thesis: contradiction

then card x <= card y1 by NAT_1:43;

then card x = card y1 by A38, A72, NAT_1:9;

hence contradiction by A19, A67, A73, CARD_2:102; :: thesis: verum

then y1,x are_c=-comparable by A5, A6, A67;

then y1 c= x by A71;

then y1 c= xm by A34, A67;

then ( y1 c= xm \/ {x1} & y1 c= xm \/ {x2} ) by A65;

hence ( y1,xm \/ {x1} are_c=-comparable & y1,xm \/ {x2} are_c=-comparable ) ; :: thesis: verum

proof

then
BS1 is simplex-like
by A12, A63, SIMPLEX0:def 20;
let y1, y2 be set ; :: according to ORDINAL1:def 8 :: thesis: ( not y1 in S1 or not y2 in S1 or y1,y2 are_c=-comparable )

assume that

A74: y1 in S1 and

A75: y2 in S1 ; :: thesis: y1,y2 are_c=-comparable

( y1 in S or y1 in {(xm \/ {x1})} ) by A74, XBOOLE_0:def 3;

then A76: ( y1 in S or y1 = xm \/ {x1} ) by TARSKI:def 1;

( y2 in S or y2 in {(xm \/ {x1})} ) by A75, XBOOLE_0:def 3;

then ( y2 in S or y2 = xm \/ {x1} ) by TARSKI:def 1;

hence y1,y2 are_c=-comparable by A66, A76, ORDINAL1:def 8; :: thesis: verum

end;assume that

A74: y1 in S1 and

A75: y2 in S1 ; :: thesis: y1,y2 are_c=-comparable

( y1 in S or y1 in {(xm \/ {x1})} ) by A74, XBOOLE_0:def 3;

then A76: ( y1 in S or y1 = xm \/ {x1} ) by TARSKI:def 1;

( y2 in S or y2 in {(xm \/ {x1})} ) by A75, XBOOLE_0:def 3;

then ( y2 in S or y2 = xm \/ {x1} ) by TARSKI:def 1;

hence y1,y2 are_c=-comparable by A66, A76, ORDINAL1:def 8; :: thesis: verum

then A77: BS1 is Simplex of (card U) - 1, BCS (Complex_of {U}) by A2, A15, A16, A20, A64, SIMPLEX0:def 18;

set SS = { S3 where S3 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S3 } ;

(center_of_mass V) .: S c= ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {(xm \/ {x1})}) by XBOOLE_1:7;

then A78: BS1 in { S3 where S3 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S3 } by A2, A46, A77;

A79: BS2 = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {(xm \/ {x2})}) by RELAT_1:120;

A80: { S3 where S3 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S3 } c= {BS1,BS2}

proof

A109:
BS2 = ((center_of_mass V) | the topology of (Complex_of {U})) .: S2
by A10, A55, RELAT_1:129;
let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in { S3 where S3 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S3 } or w in {BS1,BS2} )

reconsider n = 0 as Nat ;

assume w in { S3 where S3 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S3 } ; :: thesis: w in {BS1,BS2}

then consider W being Simplex of card S, BCS (Complex_of {U}) such that

A81: w = W and

A82: (center_of_mass V) .: S c= W ;

((card S) + n) + 1 <= card U by A2;

then consider T being finite Subset-Family of V such that

A83: T misses S and

A84: ( T \/ S is c=-linear & T \/ S is with_non-empty_elements ) and

A85: card T = n + 1 and

A86: union T c= U and

A87: @ W = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) by A1, A82, Th35;

consider x3 being object such that

A88: {x3} = T by A85, CARD_2:42;

A89: x3 in T by A88, TARSKI:def 1;

then A90: not x3 in S by A83, XBOOLE_0:3;

reconsider x3 = x3 as set by TARSKI:1;

A91: x3 c= union T by A89, ZFMISC_1:74;

A92: x3 in T \/ S by A89, XBOOLE_0:def 3;

reconsider x3 = x3 as finite Subset of U by A86, A91, XBOOLE_1:1;

A93: not xM c= x3

xM in S \/ T by A40, XBOOLE_0:def 3;

then xM,x3 are_c=-comparable by A84, A92;

then x3 c= xM by A93;

then A105: x3 \ xm c= xM \ xm by XBOOLE_1:33;

A106: xM = xm \/ xM by A41, XBOOLE_1:12;

A107: x3 \ xm <> xM \ xm

x3 \/ xm = (x3 \ xm) \/ xm by XBOOLE_1:39;

then ( x3 = xm \/ {x1} or x3 = xm \/ {x2} ) by A43, A104, A105, A107, A108, ZFMISC_1:36;

hence w in {BS1,BS2} by A79, A46, A81, A87, A88, TARSKI:def 2; :: thesis: verum

end;reconsider n = 0 as Nat ;

assume w in { S3 where S3 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S3 } ; :: thesis: w in {BS1,BS2}

then consider W being Simplex of card S, BCS (Complex_of {U}) such that

A81: w = W and

A82: (center_of_mass V) .: S c= W ;

((card S) + n) + 1 <= card U by A2;

then consider T being finite Subset-Family of V such that

A83: T misses S and

A84: ( T \/ S is c=-linear & T \/ S is with_non-empty_elements ) and

A85: card T = n + 1 and

A86: union T c= U and

A87: @ W = ((center_of_mass V) .: S) \/ ((center_of_mass V) .: T) by A1, A82, Th35;

consider x3 being object such that

A88: {x3} = T by A85, CARD_2:42;

A89: x3 in T by A88, TARSKI:def 1;

then A90: not x3 in S by A83, XBOOLE_0:3;

reconsider x3 = x3 as set by TARSKI:1;

A91: x3 c= union T by A89, ZFMISC_1:74;

A92: x3 in T \/ S by A89, XBOOLE_0:def 3;

reconsider x3 = x3 as finite Subset of U by A86, A91, XBOOLE_1:1;

A93: not xM c= x3

proof

A97:
( xm c= x3 & xm <> x3 )
consider x4 being set such that

A94: x4 in ss and

A95: card x4 = card x3 by A6, A36, A21, A84, A92, Th36, NAT_1:43;

assume xM c= x3 ; :: thesis: contradiction

then (card x) + 1 <= card x3 by A38, NAT_1:43;

then x <> x4 by A95, NAT_1:13;

then not x4 in {x} by TARSKI:def 1;

then A96: x4 in s by A9, A94, XBOOLE_0:def 5;

then x4 in S \/ T by XBOOLE_0:def 3;

then x3,x4 are_c=-comparable by A84, A92;

then ( x3 c= x4 or x4 c= x3 ) ;

hence contradiction by A90, A95, A96, CARD_2:102; :: thesis: verum

end;A94: x4 in ss and

A95: card x4 = card x3 by A6, A36, A21, A84, A92, Th36, NAT_1:43;

assume xM c= x3 ; :: thesis: contradiction

then (card x) + 1 <= card x3 by A38, NAT_1:43;

then x <> x4 by A95, NAT_1:13;

then not x4 in {x} by TARSKI:def 1;

then A96: x4 in s by A9, A94, XBOOLE_0:def 5;

then x4 in S \/ T by XBOOLE_0:def 3;

then x3,x4 are_c=-comparable by A84, A92;

then ( x3 c= x4 or x4 c= x3 ) ;

hence contradiction by A90, A95, A96, CARD_2:102; :: thesis: verum

proof
end;

then A104:
x3 = x3 \/ xm
by XBOOLE_1:12;per cases
( xm = {} or xm in s )
by A32;

end;

suppose A98:
xm in s
; :: thesis: ( xm c= x3 & xm <> x3 )

A99:
not x3 c= xm

then xm,x3 are_c=-comparable by A84, A92;

hence ( xm c= x3 & xm <> x3 ) by A99; :: thesis: verum

end;proof

xm in T \/ S
by A98, XBOOLE_0:def 3;
assume
x3 c= xm
; :: thesis: contradiction

then A100: card x3 <= card xm by NAT_1:43;

consider x4 being set such that

A101: x4 in ss and

A102: card x4 = card x3 by A6, A36, A21, A84, A92, Th36, NAT_1:43;

(card xm) + 1 = card x by A33;

then card x <> card x3 by A100, NAT_1:13;

then not x4 in {x} by A102, TARSKI:def 1;

then A103: x4 in s by A9, A101, XBOOLE_0:def 5;

then x4 in S \/ T by XBOOLE_0:def 3;

then x3,x4 are_c=-comparable by A84, A92;

then ( x3 c= x4 or x4 c= x3 ) ;

hence contradiction by A90, A102, A103, CARD_2:102; :: thesis: verum

end;then A100: card x3 <= card xm by NAT_1:43;

consider x4 being set such that

A101: x4 in ss and

A102: card x4 = card x3 by A6, A36, A21, A84, A92, Th36, NAT_1:43;

(card xm) + 1 = card x by A33;

then card x <> card x3 by A100, NAT_1:13;

then not x4 in {x} by A102, TARSKI:def 1;

then A103: x4 in s by A9, A101, XBOOLE_0:def 5;

then x4 in S \/ T by XBOOLE_0:def 3;

then x3,x4 are_c=-comparable by A84, A92;

then ( x3 c= x4 or x4 c= x3 ) ;

hence contradiction by A90, A102, A103, CARD_2:102; :: thesis: verum

then xm,x3 are_c=-comparable by A84, A92;

hence ( xm c= x3 & xm <> x3 ) by A99; :: thesis: verum

xM in S \/ T by A40, XBOOLE_0:def 3;

then xM,x3 are_c=-comparable by A84, A92;

then x3 c= xM by A93;

then A105: x3 \ xm c= xM \ xm by XBOOLE_1:33;

A106: xM = xm \/ xM by A41, XBOOLE_1:12;

A107: x3 \ xm <> xM \ xm

proof

A108:
x3 \ xm <> {}
by XBOOLE_1:37, A97;
assume
x3 \ xm = xM \ xm
; :: thesis: contradiction

then x3 = (xM \ xm) \/ xm by A104, XBOOLE_1:39;

hence contradiction by A93, A106, XBOOLE_1:39; :: thesis: verum

end;then x3 = (xM \ xm) \/ xm by A104, XBOOLE_1:39;

hence contradiction by A93, A106, XBOOLE_1:39; :: thesis: verum

x3 \/ xm = (x3 \ xm) \/ xm by XBOOLE_1:39;

then ( x3 = xm \/ {x1} or x3 = xm \/ {x2} ) by A43, A104, A105, A107, A108, ZFMISC_1:36;

hence w in {BS1,BS2} by A79, A46, A81, A87, A88, TARSKI:def 2; :: thesis: verum

A110: BS1 <> BS2

proof

S2 is c=-linear
assume A111:
BS1 = BS2
; :: thesis: contradiction

then BS1 \ BS2 = {} by XBOOLE_1:37;

then ((center_of_mass V) | the topology of (Complex_of {U})) .: (S1 \ S2) = {} by A109, A62, FUNCT_1:64;

then A112: dom ((center_of_mass V) | the topology of (Complex_of {U})) misses S1 \ S2 by RELAT_1:118;

BS2 \ BS1 = {} by A111, XBOOLE_1:37;

then ((center_of_mass V) | the topology of (Complex_of {U})) .: (S2 \ S1) = {} by A109, A62, FUNCT_1:64;

then A113: dom ((center_of_mass V) | the topology of (Complex_of {U})) misses S2 \ S1 by RELAT_1:118;

A114: dom ((center_of_mass V) | the topology of (Complex_of {U})) = (dom (center_of_mass V)) /\ the topology of (Complex_of {U}) by RELAT_1:61;

xm \/ {x1} in {(xm \/ {x1})} by TARSKI:def 1;

then A115: xm \/ {x1} in S1 by XBOOLE_0:def 3;

A116: dom (center_of_mass V) = (bool the carrier of V) \ {{}} by FUNCT_2:def 1;

A117: S1 \ S2 c= S1 by XBOOLE_1:36;

then not {} in S1 \ S2 by A1;

then A118: S1 \ S2 c= dom (center_of_mass V) by A116, ZFMISC_1:34;

A119: S2 \ S1 c= S2 by XBOOLE_1:36;

then not {} in S2 \ S1 by A1;

then A120: S2 \ S1 c= dom (center_of_mass V) by A116, ZFMISC_1:34;

S1 \ S2 c= bool U by A60, A117;

then S1 \ S2 c= dom ((center_of_mass V) | the topology of (Complex_of {U})) by A10, A114, A118, XBOOLE_1:19;

then A121: S1 \ S2 = {} by A112, XBOOLE_1:67;

S2 \ S1 c= bool U by A55, A119;

then S2 \ S1 c= dom ((center_of_mass V) | the topology of (Complex_of {U})) by A10, A114, A120, XBOOLE_1:19;

then S1 = S2 by A113, A121, XBOOLE_1:32, XBOOLE_1:67;

then xm \/ {x1} in {(xm \/ {x2})} by A49, A115, XBOOLE_0:def 3;

then A122: xm \/ {x1} = xm \/ {x2} by TARSKI:def 1;

x1 in {x1} by TARSKI:def 1;

then x1 in xm \/ {x1} by XBOOLE_0:def 3;

then x1 in {x2} by A47, A122, XBOOLE_0:def 3;

hence contradiction by A42, TARSKI:def 1; :: thesis: verum

end;then BS1 \ BS2 = {} by XBOOLE_1:37;

then ((center_of_mass V) | the topology of (Complex_of {U})) .: (S1 \ S2) = {} by A109, A62, FUNCT_1:64;

then A112: dom ((center_of_mass V) | the topology of (Complex_of {U})) misses S1 \ S2 by RELAT_1:118;

BS2 \ BS1 = {} by A111, XBOOLE_1:37;

then ((center_of_mass V) | the topology of (Complex_of {U})) .: (S2 \ S1) = {} by A109, A62, FUNCT_1:64;

then A113: dom ((center_of_mass V) | the topology of (Complex_of {U})) misses S2 \ S1 by RELAT_1:118;

A114: dom ((center_of_mass V) | the topology of (Complex_of {U})) = (dom (center_of_mass V)) /\ the topology of (Complex_of {U}) by RELAT_1:61;

xm \/ {x1} in {(xm \/ {x1})} by TARSKI:def 1;

then A115: xm \/ {x1} in S1 by XBOOLE_0:def 3;

A116: dom (center_of_mass V) = (bool the carrier of V) \ {{}} by FUNCT_2:def 1;

A117: S1 \ S2 c= S1 by XBOOLE_1:36;

then not {} in S1 \ S2 by A1;

then A118: S1 \ S2 c= dom (center_of_mass V) by A116, ZFMISC_1:34;

A119: S2 \ S1 c= S2 by XBOOLE_1:36;

then not {} in S2 \ S1 by A1;

then A120: S2 \ S1 c= dom (center_of_mass V) by A116, ZFMISC_1:34;

S1 \ S2 c= bool U by A60, A117;

then S1 \ S2 c= dom ((center_of_mass V) | the topology of (Complex_of {U})) by A10, A114, A118, XBOOLE_1:19;

then A121: S1 \ S2 = {} by A112, XBOOLE_1:67;

S2 \ S1 c= bool U by A55, A119;

then S2 \ S1 c= dom ((center_of_mass V) | the topology of (Complex_of {U})) by A10, A114, A120, XBOOLE_1:19;

then S1 = S2 by A113, A121, XBOOLE_1:32, XBOOLE_1:67;

then xm \/ {x1} in {(xm \/ {x2})} by A49, A115, XBOOLE_0:def 3;

then A122: xm \/ {x1} = xm \/ {x2} by TARSKI:def 1;

x1 in {x1} by TARSKI:def 1;

then x1 in xm \/ {x1} by XBOOLE_0:def 3;

then x1 in {x2} by A47, A122, XBOOLE_0:def 3;

hence contradiction by A42, TARSKI:def 1; :: thesis: verum

proof

then
BS2 is simplex-like
by A12, A57, SIMPLEX0:def 20;
let y1, y2 be set ; :: according to ORDINAL1:def 8 :: thesis: ( not y1 in S2 or not y2 in S2 or y1,y2 are_c=-comparable )

assume that

A123: y1 in S2 and

A124: y2 in S2 ; :: thesis: y1,y2 are_c=-comparable

( y1 in S or y1 in {(xm \/ {x2})} ) by A123, XBOOLE_0:def 3;

then A125: ( y1 in S or y1 = xm \/ {x2} ) by TARSKI:def 1;

( y2 in S or y2 in {(xm \/ {x2})} ) by A124, XBOOLE_0:def 3;

then ( y2 in S or y2 = xm \/ {x2} ) by TARSKI:def 1;

hence y1,y2 are_c=-comparable by A66, A125, ORDINAL1:def 8; :: thesis: verum

end;assume that

A123: y1 in S2 and

A124: y2 in S2 ; :: thesis: y1,y2 are_c=-comparable

( y1 in S or y1 in {(xm \/ {x2})} ) by A123, XBOOLE_0:def 3;

then A125: ( y1 in S or y1 = xm \/ {x2} ) by TARSKI:def 1;

( y2 in S or y2 in {(xm \/ {x2})} ) by A124, XBOOLE_0:def 3;

then ( y2 in S or y2 = xm \/ {x2} ) by TARSKI:def 1;

hence y1,y2 are_c=-comparable by A66, A125, ORDINAL1:def 8; :: thesis: verum

then A126: BS2 is Simplex of (card U) - 1, BCS (Complex_of {U}) by A2, A15, A16, A20, A58, SIMPLEX0:def 18;

(center_of_mass V) .: S c= ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {(xm \/ {x2})}) by XBOOLE_1:7;

then BS2 in { S3 where S3 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S3 } by A2, A79, A126;

then {BS1,BS2} c= { S3 where S3 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S3 } by A78, ZFMISC_1:32;

then { S3 where S3 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S3 } = {BS1,BS2} by A80;

hence card { S1 where S1 is Simplex of card S, BCS (Complex_of {(union S)}) : (center_of_mass V) .: S c= S1 } = 2 by A110, CARD_2:57; :: thesis: verum