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

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

hence
diameter P = 0
by A1, Def8; :: thesis: verum
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

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;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 s be Real; :: thesis: ( ( for x, y being Point of T st x in P & y in P holds
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;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

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