let X be set ; :: thesis: for R, T being Tolerance of X st TolClasses R c= TolClasses T holds
R c= T
let R, T be Tolerance of X; :: thesis: ( TolClasses R c= TolClasses T implies R c= T )
assume A1: TolClasses R c= TolClasses T ; :: thesis: R c= T
let x be set ; :: according to RELAT_1:def 3 :: thesis: for b₁ being set holds
( not [x,b₁] in R or [x,b₁] in T )
let y be set ; :: thesis: ( not [x,y] in R or [x,y] in T )
assume [x,y] in R ; :: thesis: [x,y] in T
then consider Z being TolClass of R such that
A2: ( x in Z & y in Z ) by Th46;
Z in TolClasses R by Def7;
then Z is TolSet of T by A1, Def7;
hence [x,y] in T by A2, Def3; :: thesis: verum