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 00 = {} as TolClass of T ;
assume T <> {} ; :: thesis: contradiction
then consider x, y being set such that
A1: [x,y] in T by RELAT_1:37;
x in X by A1, ZFMISC_1:87;
then ex z being set st
( z in 00 & not [x,z] in T ) by Def4;
hence contradiction ; :: thesis: verum