let T be non empty Reflexive symmetric triangle MetrStruct ; :: thesis: for x being set
for P being Subset of T st P = {x} holds
diameter P = 0
let x be set ; :: thesis: for P being Subset of T st P = {x} holds
diameter P = 0
let P be Subset of T; :: thesis: ( P = {x} implies diameter P = 0 )
assume A1: P = {x} ; :: thesis: diameter P = 0
then A2: x in P by TARSKI:def 1;
then reconsider t1 = x as Element of T ;
( ( for x, y being Point of T st x in P & y in P holds
dist (x,y) <= 0 ) & ( for s being Real st ( for x, y being Point of T st x in P & y in P holds
dist (x,y) <= s ) holds
0 <= s ) )

proof

thus for x, y being Point of T st x in P & y in P holds
dist (x,y) <= 0 :: thesis: for s being Real st ( for x, y being Point of T st x in P & y in P holds
dist (x,y) <= s ) holds
0 <= s

proof

let x, y be Point of T; :: thesis: ( x in P & y in P implies dist (x,y) <= 0 )
assume that
A3: x in P and
A4: y in P ; :: thesis: dist (x,y) <= 0
x = t1 by A1, A3, TARSKI:def 1;
then dist (x,y) = dist (t1,t1) by A1, A4, TARSKI:def 1
.= 0 by METRIC_1:1 ;
hence dist (x,y) <= 0 ; :: thesis: verum

end;

let s be Real; :: thesis: ( ( for x, y being Point of T st x in P & y in P holds
dist (x,y) <= s ) implies 0 <= s )
assume for x, y being Point of T st x in P & y in P holds
dist (x,y) <= s ; :: thesis: 0 <= s
then dist (t1,t1) <= s by A2;
hence 0 <= s by METRIC_1:1; :: thesis: verum

end;

hence diameter P = 0 by A1, Def8; :: thesis: verum