let X be set ; :: thesis: for R, T being Tolerance of X holds
( TolSets R c= TolSets T iff R c= T )
let R, T be Tolerance of X; :: thesis: ( TolSets R c= TolSets T iff R c= T )
thus ( TolSets R c= TolSets T implies R c= T ) :: thesis: ( R c= T implies TolSets R c= TolSets T )

proof

assume A1: TolSets R c= TolSets 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 TolSets R by Def6;
then Z is TolSet of T by A1, Def6;
hence [x,y] in T by A2, Def3; :: thesis: verum

end;

assume A3: R c= T ; :: thesis: TolSets R c= TolSets T
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in TolSets R or x in TolSets T )
assume x in TolSets R ; :: thesis: x in TolSets T
then reconsider Z = x as TolSet of R by Def6;
for x, y being set st x in Z & y in Z holds
[x,y] in T

proof

let x, y be set ; :: thesis: ( x in Z & y in Z implies [x,y] in T )
assume ( x in Z & y in Z ) ; :: thesis: [x,y] in T
then [x,y] in R by Def3;
hence [x,y] in T by A3; :: thesis: verum

end;

then Z is TolSet of T by Def3;
hence x in TolSets T by Def6; :: thesis: verum