let X be set ; :: thesis: for T being Tolerance of X
for x being set st x in X holds
ex Z being TolClass of T st x in Z
let T be Tolerance of X; :: thesis: for x being set st x in X holds
ex Z being TolClass of T st x in Z
let x be set ; :: thesis: ( x in X implies ex Z being TolClass of T st x in Z )
assume x in X ; :: thesis: ex Z being TolClass of T st x in Z
then [x,x] in T by Th7;
then ex Z being TolClass of T st
( x in Z & x in Z ) by Th20;
hence ex Z being TolClass of T st x in Z ; :: thesis: verum