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

assume A1: ( a >= diameter ([#] M) & R = (dist_toler (M,a)) [*] ) ; :: thesis: Class R = { the carrier of M}

Class (nabla the carrier of M) = { the carrier of M} by MSUALG_9:4;

hence Class R = { the carrier of M} by A1, Th39; :: thesis: verum

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

assume A1: ( a >= diameter ([#] M) & R = (dist_toler (M,a)) [*] ) ; :: thesis: Class R = { the carrier of M}

Class (nabla the carrier of M) = { the carrier of M} by MSUALG_9:4;

hence Class R = { the carrier of M} by A1, Th39; :: thesis: verum