let X be set ; :: thesis: for R being Tolerance of X
for x being set st x in X holds
x in Class (R,x)
let R be Tolerance of X; :: thesis: for x being set st x in X holds
x in Class (R,x)
let x be set ; :: thesis: ( x in X implies x in Class (R,x) )
assume x in X ; :: thesis: x in Class (R,x)
then [x,x] in R by Th11;
hence x in Class (R,x) by Th27; :: thesis: verum