let X be set ; :: thesis: for T being Tolerance of X
for Y, Z being set st Y is TolSet of T holds
Y /\ Z is TolSet of T
let T be Tolerance of X; :: thesis: for Y, Z being set st Y is TolSet of T holds
Y /\ Z is TolSet of T
let Y, Z be set ; :: thesis: ( Y is TolSet of T implies Y /\ Z is TolSet of T )
assume A1: Y is TolSet of T ; :: thesis: Y /\ Z is TolSet of T
let x be set ; :: according to TOLER_1:def 1 :: thesis: for y being set st x in Y /\ Z & y in Y /\ Z holds
[x,y] in T
let y be set ; :: thesis: ( x in Y /\ Z & y in Y /\ Z implies [x,y] in T )
assume ( x in Y /\ Z & y in Y /\ Z ) ; :: thesis: [x,y] in T
then ( x in Y & y in Y ) by XBOOLE_0:def 4;
hence [x,y] in T by A1, Def1; :: thesis: verum