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:
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 ;
then dist (x,y) = dist (t1,t1) by
.= 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 ; :: thesis: verum