let M be non empty Reflexive symmetric bounded MetrStruct ; :: thesis: for R being Equivalence_Relation of M
for a being non negative Real st a >= diameter ([#] M) & R = (dist_toler (M,a)) [*] holds
Class R = { the carrier of M}
let R be Equivalence_Relation of M; :: thesis: for a being non negative Real st a >= diameter ([#] M) & R = (dist_toler (M,a)) [*] holds
Class R = { the carrier of M}
let a be non negative Real; :: thesis: ( a >= diameter ([#] M) & R = (dist_toler (M,a)) [*] implies Class R = { the carrier of M} )
Class (nabla the carrier of M) = { the carrier of M} by MSUALG_9:4;
hence ( a >= diameter ([#] M) & R = (dist_toler (M,a)) [*] implies Class R = { the carrier of M} ) by Th39; :: thesis: verum