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

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