theorem Th20: :: TOLER_1:20

for X being set
for T being Tolerance of X
for x, y being object st [x,y] in T holds
ex Z being TolClass of T st
( x in Z & y in Z )