let A be non empty convex Subset of (TOP-REAL 3); :: thesis: for n, u, v being Element of (TOP-REAL 3) st ( for w being Element of (TOP-REAL 3) st w in A holds
|(n,w)| <> 0 ) & u in A & v in A holds
0 < |(n,u)| * |(n,v)|
let n, u, v be Element of (TOP-REAL 3); :: thesis: ( ( for w being Element of (TOP-REAL 3) st w in A holds
|(n,w)| <> 0 ) & u in A & v in A implies 0 < |(n,u)| * |(n,v)| )
assume that
A1: for w being Element of (TOP-REAL 3) st w in A holds
|(n,w)| <> 0 and
A2: ( u in A & v in A ) ; :: thesis: 0 < |(n,u)| * |(n,v)|
set x = |(n,u)|;
set y = |(n,v)|;
assume A3: not 0 < |(n,u)| * |(n,v)| ; :: thesis: contradiction
A4: ( |(n,u)| <> 0 & |(n,v)| <> 0 ) by A1, A2;
then A5: ( 0 < |(n,u)| / (|(n,u)| - |(n,v)|) & |(n,u)| / (|(n,u)| - |(n,v)|) < 1 ) by A3, BKMODEL3:1;
reconsider l = |(n,u)| / (|(n,u)| - |(n,v)|) as non zero Real by A3, A4, BKMODEL3:1;
reconsider w = (l * v) + ((1 - l) * u) as Element of (TOP-REAL 3) ;
|(n,u)| <> |(n,v)|
proof
assume |(n,u)| = |(n,v)| ; :: thesis: contradiction
then l = 0 by XCMPLX_1:49;
hence contradiction ; :: thesis: verum
end;
then A6: 1 - l = - (|(n,v)| / (|(n,u)| - |(n,v)|)) by Th25;
|(n,w)| = 0
proof
|(n,w)| = |(n,(l * v))| + |(n,((1 - l) * u))| by EUCLID_2:26
.= (l * |(n,v)|) + |(n,((1 - l) * u))| by EUCLID_2:19
.= ((|(n,u)| / (|(n,u)| - |(n,v)|)) * |(n,v)|) + (((- |(n,v)|) / (|(n,u)| - |(n,v)|)) * |(n,u)|) by A6, EUCLID_2:19 ;
hence |(n,w)| = 0 ; :: thesis: verum
end;
hence contradiction by A1, A2, A5, CONVEX1:def 2; :: thesis: verum