let x be set ; :: thesis: for V being RealLinearSpace
for A being affinely-independent Subset of V st |-- (A,x) = ([#] V) --> 0 holds
not x in A
let V be RealLinearSpace; :: thesis: for A being affinely-independent Subset of V st |-- (A,x) = ([#] V) --> 0 holds
not x in A
let A be affinely-independent Subset of V; :: thesis: ( |-- (A,x) = ([#] V) --> 0 implies not x in A )
set Ax = |-- (A,x);
assume A1: |-- (A,x) = ([#] V) --> 0 ; :: thesis: not x in A
A2: A c= conv A by RLAFFIN1:2;
assume A3: x in A ; :: thesis: contradiction
then 0 = (|-- (A,x)) . x by A1, FUNCOP_1:7
.= (x |-- A) . x by A3, Def3
.= 1 by A3, A2, RLAFFIN1:72 ;
hence contradiction ; :: thesis: verum