let Y, X 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 set ; :: 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, Def3;
hence x in X by Th27; :: thesis: verum