let X, Y be set ; :: thesis: for T being Tolerance of X st Y is TolSet of T holds
Y c= X
let T be Tolerance of X; :: thesis: ( Y is TolSet of T implies Y c= X )
assume A1: Y is TolSet of T ; :: thesis: Y c= X
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in X )
assume x in Y ; :: thesis: x in X
then [x,x] in T by A1, Def1;
hence x in X by Th7; :: thesis: verum