let X be set ; :: thesis: for T being Tolerance of X
for x being set st x in X holds
{x} is TolSet of T
let T be Tolerance of X; :: thesis: for x being set st x in X holds
{x} is TolSet of T
let x be set ; :: thesis: ( x in X implies {x} is TolSet of T )
assume x in X ; :: thesis: {x} is TolSet of T
then [x,x] in T by Th7;
then {x,x} is TolSet of T by Th15;
hence {x} is TolSet of T by ENUMSET1:29; :: thesis: verum