let X, Y be set ; :: thesis: for T being Tolerance of X st Y c= X holds
T |_2 Y is Tolerance of Y
let T be Tolerance of X; :: thesis: ( Y c= X implies T |_2 Y is Tolerance of Y )
assume Y c= X ; :: thesis: T |_2 Y is Tolerance of Y
then reconsider Z = Y as Subset of X ;
T |_2 Z is Tolerance of Z ;
hence T |_2 Y is Tolerance of Y ; :: thesis: verum