let X be set ; :: thesis: for T being Tolerance of X holds {} is TolSet of T
let T be Tolerance of X; :: thesis: {} is TolSet of T
let x be set ; :: according to TOLER_1:def 3 :: thesis: for y being set st x in {} & y in {} holds
[x,y] in T
let y be set ; :: thesis: ( x in {} & y in {} implies [x,y] in T )
assume ( x in {} & y in {} ) ; :: thesis: [x,y] in T
hence [x,y] in T ; :: thesis: verum