set ff = SteinhausGen (f,p);
for a, b being Element of X holds (SteinhausGen (f,p)) . (a,b) = (SteinhausGen (f,p)) . (b,a)

proof

let a, b be Element of X; :: thesis: (SteinhausGen (f,p)) . (a,b) = (SteinhausGen (f,p)) . (b,a)
(SteinhausGen (f,p)) . (a,b) = (2 * (f . (a,b))) / (((f . (a,p)) + (f . (b,p))) + (f . (a,b))) by SteinGen
.= (2 * (f . (b,a))) / (((f . (a,p)) + (f . (b,p))) + (f . (a,b))) by METRIC_1:def 4
.= (2 * (f . (b,a))) / (((f . (b,p)) + (f . (a,p))) + (f . (b,a))) by METRIC_1:def 4
.= (SteinhausGen (f,p)) . (b,a) by SteinGen ;
hence (SteinhausGen (f,p)) . (a,b) = (SteinhausGen (f,p)) . (b,a) ; :: thesis: verum

end;

hence SteinhausGen (f,p) is symmetric by METRIC_1:def 4; :: thesis: verum