let V be RealLinearSpace; :: thesis: for If being finite affinely-independent Subset of V st not If is empty holds
(center_of_mass V) . If in Int If
let If be finite affinely-independent Subset of V; :: thesis: ( not If is empty implies (center_of_mass V) . If in Int If )
set BA = ((center_of_mass V) . If) |-- If;
A1: If c= Carrier (((center_of_mass V) . If) |-- If)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in If or x in Carrier (((center_of_mass V) . If) |-- If) )
assume A2: x in If ; :: thesis: x in Carrier (((center_of_mass V) . If) |-- If)
then (((center_of_mass V) . If) |-- If) . x = 1 / (card If) by Th18;
hence x in Carrier (((center_of_mass V) . If) |-- If) by A2; :: thesis: verum
end;
assume not If is empty ; :: thesis: (center_of_mass V) . If in Int If
then A3: (center_of_mass V) . If in conv If by Th16;
Carrier (((center_of_mass V) . If) |-- If) c= If by RLVECT_2:def 6;
then ( Carrier (((center_of_mass V) . If) |-- If) = If & ((center_of_mass V) . If) |-- If is convex ) by A1, A3, RLAFFIN1:71;
then ( conv If c= Affin If & Sum (((center_of_mass V) . If) |-- If) in Int If ) by Th12, RLAFFIN1:65;
hence (center_of_mass V) . If in Int If by A3, RLAFFIN1:def 7; :: thesis: verum