let X be set ; :: thesis: for T, R being Tolerance of X st TolClasses T = TolClasses R holds
T = R
let T, R be Tolerance of X; :: thesis: ( TolClasses T = TolClasses R implies T = R )
assume A1: TolClasses T = TolClasses R ; :: thesis: T = R
for Z being set holds
( Z is TolClass of T iff Z is TolClass of R )
proof
let Z be set ; :: thesis: ( Z is TolClass of T iff Z is TolClass of R )
( Z is TolClass of T iff Z in TolClasses R ) by A1, Def4;
hence ( Z is TolClass of T iff Z is TolClass of R ) by Def4; :: thesis: verum
end;
hence T = R by Th26; :: thesis: verum