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 1 :: 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 that
A1: x in {} and
y in {} ; :: thesis: [x,y] in T
thus [x,y] in T by A1; :: thesis: verum