let X be set ; :: thesis: for T, R being Tolerance of X st TolClasses R c= TolClasses T holds
R c= T
let T, R 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, y be object ; :: according to RELAT_1:def 3 :: 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 Th20;
Z in TolClasses R by Def4;
then Z is TolSet of T by A1, Def4;
hence [x,y] in T by A2, Def1; :: thesis: verum