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 = 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

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, 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

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