let X be set ; :: thesis: for R being Tolerance of X

for x being object st x in X holds

x in Class (R,x)

let R be Tolerance of X; :: thesis: for x being object st x in X holds

x in Class (R,x)

let x be object ; :: 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 Th5;

hence x in Class (R,x) by Th19; :: thesis: verum

for x being object st x in X holds

x in Class (R,x)

let R be Tolerance of X; :: thesis: for x being object st x in X holds

x in Class (R,x)

let x be object ; :: 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 Th5;

hence x in Class (R,x) by Th19; :: thesis: verum