let X be set ; :: thesis: for T being Tolerance of X st {} is TolClass of T holds
T = {}
let T be Tolerance of X; :: thesis: ( {} is TolClass of T implies T = {} )
assume {} is TolClass of T ; :: thesis: T = {}
then reconsider O0 = {} as TolClass of T ;
assume T <> {} ; :: thesis: contradiction
then consider x, y being object such that
A1: [x,y] in T ;
x in X by A1, ZFMISC_1:87;
then ex z being set st
( z in O0 & not [x,z] in T ) by Def2;
hence contradiction ; :: thesis: verum