reconsider ZS = {0} as non empty set ;
deffunc H1( Element of ZS, Element of ZS) -> Element of REAL = In (0,REAL);
consider F being Function of [:ZS,ZS:],REAL such that
A1: for x, y being Element of ZS holds F . (x,y) = H1(x,y) from BINOP_1:sch 4();
 reconsider V = MetrStruct(# ZS,F #) as non empty MetrStruct ;
A2: now :: thesis: for a, b being Element of V holds dist (a,b) = dist (b,a)
let a, b be Element of V; :: thesis: dist (a,b) = dist (b,a)
thus dist (a,b) = F . (a,b) by METRIC_1:def 1
.= 0 by A1
.= F . (b,a) by A1
.= dist (b,a) by METRIC_1:def 1 ; :: thesis: verum
end;
A3: now :: thesis: for a being Element of V holds dist (a,a) = 0
let a be Element of V; :: thesis: dist (a,a) = 0
thus dist (a,a) = F . (a,a) by METRIC_1:def 1
.= 0 by A1 ; :: thesis: verum
end;
A4: now :: thesis: for a, b, c being Element of V holds dist (a,c) <= (dist (a,b)) + (dist (b,c))
let a, b, c be Element of V; :: thesis: dist (a,c) <= (dist (a,b)) + (dist (b,c))
A5: c = 0 by TARSKI:def 1;
a = 0 by TARSKI:def 1;
then ( b = 0 & dist (a,c) = 0 ) by A3, A5, TARSKI:def 1;
hence dist (a,c) <= (dist (a,b)) + (dist (b,c)) by A3, A5; :: thesis: verum
end;
now :: thesis: for a, b being Element of V st dist (a,b) = 0 holds
a = b
let a, b be Element of V; :: thesis: ( dist (a,b) = 0 implies a = b )
assume dist (a,b) = 0 ; :: thesis: a = b
a = 0 by TARSKI:def 1;
hence a = b by TARSKI:def 1; :: thesis: verum
end;
then reconsider V = V as non empty Reflexive discerning symmetric triangle MetrStruct by A3, A2, A4, METRIC_1:1, METRIC_1:2, METRIC_1:3, METRIC_1:4;
take V ; :: thesis: V is convex
let x, y be Element of V; :: according to VECTMETR:def 1 :: thesis: for r being Real st 0 <= r & r <= 1 holds
ex z being Element of V st
( dist (x,z) = r * (dist (x,y)) & dist (z,y) = (1 - r) * (dist (x,y)) )
let r be Real; :: thesis: ( 0 <= r & r <= 1 implies ex z being Element of V st
( dist (x,z) = r * (dist (x,y)) & dist (z,y) = (1 - r) * (dist (x,y)) ) )
assume that
0 <= r and
r <= 1 ; :: thesis: ex z being Element of V st
( dist (x,z) = r * (dist (x,y)) & dist (z,y) = (1 - r) * (dist (x,y)) )
take z = x; :: thesis: ( dist (x,z) = r * (dist (x,y)) & dist (z,y) = (1 - r) * (dist (x,y)) )
A6: dist (z,y) = F . (z,y) by METRIC_1:def 1
.= 0 by A1 ;
dist (x,z) = F . (x,z) by METRIC_1:def 1
.= 0 by A1 ;
hence ( dist (x,z) = r * (dist (x,y)) & dist (z,y) = (1 - r) * (dist (x,y)) ) by A6; :: thesis: verum