let M be non empty Reflexive symmetric MetrStruct ; :: thesis: for r being Real st r > 0 holds
ex A being Subset of M st
( ( for p, q being Point of M st p <> q & p in A & q in A holds
dist (p,q) >= r ) & ( for p being Point of M ex q being Point of M st
( q in A & p in Ball (q,r) ) ) )
let r be Real; :: thesis: ( r > 0 implies ex A being Subset of M st
( ( for p, q being Point of M st p <> q & p in A & q in A holds
dist (p,q) >= r ) & ( for p being Point of M ex q being Point of M st
( q in A & p in Ball (q,r) ) ) ) )
assume A1: r > 0 ; :: thesis: ex A being Subset of M st
( ( for p, q being Point of M st p <> q & p in A & q in A holds
dist (p,q) >= r ) & ( for p being Point of M ex q being Point of M st
( q in A & p in Ball (q,r) ) ) )
set cM = the carrier of M;
defpred S₁[ set , set ] means for p, q being Point of M st p = $1 & q = $2 holds
dist (p,q) >= r;
A2: for x being Element of the carrier of M holds not S₁[x,x] A3: for x, y being Element of the carrier of M holds
( S₁[x,y] iff S₁[y,x] ) ;
consider A being Subset of the carrier of M such that
A4: for x, y being Element of the carrier of M st x in A & y in A & x <> y holds
S₁[x,y] and
A5: for x being Element of the carrier of M ex y being Element of the carrier of M st
( y in A & not S₁[x,y] ) from COMPL_SP:sch 2(A3, A2);
take A ; :: thesis: ( ( for p, q being Point of M st p <> q & p in A & q in A holds
dist (p,q) >= r ) & ( for p being Point of M ex q being Point of M st
( q in A & p in Ball (q,r) ) ) )
thus for p, q being Point of M st p <> q & p in A & q in A holds
dist (p,q) >= r by A4; :: thesis: for p being Point of M ex q being Point of M st
( q in A & p in Ball (q,r) )
let p be Point of M; :: thesis: ex q being Point of M st
( q in A & p in Ball (q,r) )
consider y being Element of the carrier of M such that
A6: y in A and
A7: not S₁[p,y] by A5;
take y ; :: thesis: ( y in A & p in Ball (y,r) )
thus ( y in A & p in Ball (y,r) ) by A6, A7, METRIC_1:11; :: thesis: verum