let X be set ; 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 ; for T being Tolerance of X st x in Class (T,y) holds
y in Class (T,x)
let T be Tolerance of X; ( x in Class (T,y) implies y in Class (T,x) )
assume
x in Class (T,y)
; 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; verum