let X be set ; for T, R being Tolerance of X st TolClasses R c= TolClasses T holds
R c= T
let T, R be Tolerance of X; ( TolClasses R c= TolClasses T implies R c= T )
assume A1:
TolClasses R c= TolClasses T
; R c= T
let x, y be object ; RELAT_1:def 3 ( not [x,y] in R or [x,y] in T )
assume
[x,y] in R
; [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; verum