reconsider ZS = {0 } as non empty set ;
deffunc H₁( Element of ZS, Element of ZS) -> Element of NAT = 0 ;
consider F being Function of [:ZS,ZS:],REAL such that
A1: for x, y being Element of ZS holds F . x,y = H₁(x,y) from BINOP_1:sch 4();
reconsider V = MetrStruct(# ZS,F #) as non empty MetrStruct ;

A2: now

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 & b = 0 ) by TARSKI:def 1;
hence a = b ; :: thesis: verum

end;

A3: now

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

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;

now

let a, b, c be Element of V; :: thesis: dist a,c <= (dist a,b) + (dist b,c)
( a = 0 & b = 0 & c = 0 ) by TARSKI:def 1;
then ( dist a,c = 0 & dist a,b = 0 & dist b,c = 0 ) by A3;
hence dist a,c <= (dist a,b) + (dist b,c) ; :: thesis: verum

end;

then reconsider V = V as non empty Reflexive discerning symmetric triangle MetrStruct by A2, A3, 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) )
A5: dist x,z = F . x,z by METRIC_1:def 1
.= 0 by A1 ;
dist z,y = F . z,y 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 A5; :: thesis: verum