let X, x, y be set ; :: thesis: for T being Tolerance of X st x in Class (T,y) holds
y in Class (T,x)
let T be Tolerance of X; :: thesis: ( x in Class (T,y) implies y in Class (T,x) )
assume x in Class (T,y) ; :: thesis: y in Class (T,x)
then [x,y] in T by EQREL_1:27;
then [y,x] in T by EQREL_1:12;
hence y in Class (T,x) by EQREL_1:27; :: thesis: verum