let X be set ; :: thesis: for x, y being object
for T being Tolerance of X st x in Class (T,y) holds
y in Class (T,x)
let x, y be object ; :: 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:19;
then [y,x] in T by EQREL_1:6;
hence y in Class (T,x) by EQREL_1:19; :: thesis: verum