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